case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
⊢ ↑↑μ E = ∫⁻ (ω : Ω), ↑(indicator E (fun x => 1) ω) ∂μ
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑(↑(fs n) ω) ∂μ) L (𝓝 (↑↑μ E))
convert FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
aux : ∀ (ω : Ω), indicator E (fun x => 1) ω = ↑(indicator E (fun x => 1) ω)
⊢ ↑↑μ E = ∫⁻ (ω : Ω), ↑(indicator E (fun x => 1) ω) ∂μ
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
⊢ ↑↑μ E = ∫⁻ (ω : Ω), ↑(indicator E (fun x => 1) ω) ∂μ
have aux : ∀ ω, indicator E (fun _ => (1 : ℝ≥0∞)) ω = ↑(indicator E (fun _ => (1 : ℝ≥0)) ω) :=
  fun ω => by simp only [ENNReal.coe_indicator, ENNReal.coe_one]
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
aux : ∀ (ω : Ω), indicator E (fun x => 1) ω = ↑(indicator E (fun x => 1) ω)
⊢ ↑↑μ E = ∫⁻ (x : Ω) in E, 1 ∂μ
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
aux : ∀ (ω : Ω), indicator E (fun x => 1) ω = ↑(indicator E (fun x => 1) ω)
⊢ ↑↑μ E = ∫⁻ (ω : Ω), ↑(indicator E (fun x => 1) ω) ∂μ
simp_rw [← aux, lintegral_indicator _ E_mble]
no goals
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
aux : ∀ (ω : Ω), indicator E (fun x => 1) ω = ↑(indicator E (fun x => 1) ω)
⊢ ↑↑μ E = ∫⁻ (x : Ω) in E, 1 ∂μ
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
no goals
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝³ : IsCountablyGenerated L
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (indicator E (fun x => 1) ω))
ω : Ω
⊢ indicator E (fun x => 1) ω = ↑(indicator E (fun x => 1) ω)
simp only [ENNReal.coe_indicator, ENNReal.coe_one]