Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), ↑(fs n) ω ≤ c
fs_lim : Tendsto (fun n => ↑(fs n)) atTop (𝓝 (indicator E fun x => 1))
fs_lim' : ∀ (ω : Ω), Tendsto (fun n => ↑(fs n) ω) atTop (𝓝 (indicator E (fun x => 1) ω))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑(↑(fs n) ω) ∂μ) atTop (𝓝 (↑↑μ E))
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), ↑(fs n) ω ≤ c
fs_lim : Tendsto (fun n => ↑(fs n)) atTop (𝓝 (indicator E fun x => 1))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑(↑(fs n) ω) ∂μ) atTop (𝓝 (↑↑μ E))
have fs_lim' :
  ∀ ω, Tendsto (fun n : ℕ => (fs n ω : ℝ≥0)) atTop (𝓝 (indicator E (fun _ => (1 : ℝ≥0)) ω)) := by
  rw [tendsto_pi_nhds] at fs_lim
  exact fun ω => fs_lim ω
no goals
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), ↑(fs n) ω ≤ c
fs_lim : Tendsto (fun n => ↑(fs n)) atTop (𝓝 (indicator E fun x => 1))
fs_lim' : ∀ (ω : Ω), Tendsto (fun n => ↑(fs n) ω) atTop (𝓝 (indicator E (fun x => 1) ω))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑(↑(fs n) ω) ∂μ) atTop (𝓝 (↑↑μ E))
apply measure_of_cont_bdd_of_tendsto_filter_indicator μ E_mble fs
  (eventually_of_forall fun n => eventually_of_forall (fs_bdd n)) (eventually_of_forall fs_lim')
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), ↑(fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i => ↑(fs i) x) atTop (𝓝 (indicator E (fun x => 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n => ↑(fs n) ω) atTop (𝓝 (indicator E (fun x => 1) ω))
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), ↑(fs n) ω ≤ c
fs_lim : Tendsto (fun n => ↑(fs n)) atTop (𝓝 (indicator E fun x => 1))
⊢ ∀ (ω : Ω), Tendsto (fun n => ↑(fs n) ω) atTop (𝓝 (indicator E (fun x => 1) ω))
rw [tendsto_pi_nhds] at fs_lim
no goals
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), ↑(fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i => ↑(fs i) x) atTop (𝓝 (indicator E (fun x => 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n => ↑(fs n) ω) atTop (𝓝 (indicator E (fun x => 1) ω))
exact fun ω => fs_lim ω