Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
⊢ Tendsto μs F (𝓝 μ)
apply (@tendsto_iff_forall_lintegral_tendsto Ω _ _ _ γ F μs μ).mpr
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
intro f
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
⊢ Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
have key :=
  @ENNReal.tendsto_toReal_iff _ F _
    (fun i => (lintegral_lt_top_of_boundedContinuous_to_nnreal (μs i : Measure Ω) f).ne) _
    (lintegral_lt_top_of_boundedContinuous_to_nnreal (μ : Measure Ω) f).ne
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
⊢ Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
⊢ Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
simp only [ENNReal.ofReal_coe_nnreal] at key
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
⊢ Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
apply key.mp
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have lip : LipschitzWith 1 ((↑) : ℝ≥0 → ℝ) := isometry_subtype_coe.lipschitz
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := by rfl
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have f₀_nn : 0 ≤ ⇑f₀ := fun _ => by
  simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have f₀_ae_nn : 0 ≤ᵐ[(μ : Measure Ω)] ⇑f₀ := eventually_of_forall f₀_nn
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have f₀_ae_nns : ∀ i, 0 ≤ᵐ[(μs i : Measure Ω)] ⇑f₀ := fun i => eventually_of_forall f₀_nn
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
aux : (∫ (a : Ω), ↑f₀ a ∂↑μ) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (↑f₀ a) ∂↑μ)
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have aux :=
  integral_eq_lintegral_of_nonneg_ae f₀_ae_nn f₀.continuous.measurable.aestronglyMeasurable
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
aux : (∫ (a : Ω), ↑f₀ a ∂↑μ) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (↑f₀ a) ∂↑μ)
auxs : ∀ (i : γ), (∫ (a : Ω), ↑f₀ a ∂↑(μs i)) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (↑f₀ a) ∂↑(μs i))
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
aux : (∫ (a : Ω), ↑f₀ a ∂↑μ) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (↑f₀ a) ∂↑μ)
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
have auxs := fun i =>
  integral_eq_lintegral_of_nonneg_ae (f₀_ae_nns i) f₀.continuous.measurable.aestronglyMeasurable
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
aux : (∫ (a : Ω), ↑(↑f a) ∂↑μ) = ENNReal.toReal (∫⁻ (a : Ω), ↑(↑f a) ∂↑μ)
auxs : ∀ (i : γ), (∫ (a : Ω), ↑(↑f a) ∂↑(μs i)) = ENNReal.toReal (∫⁻ (a : Ω), ↑(↑f a) ∂↑(μs i))
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
aux : (∫ (a : Ω), ↑f₀ a ∂↑μ) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (↑f₀ a) ∂↑μ)
auxs : ∀ (i : γ), (∫ (a : Ω), ↑f₀ a ∂↑(μs i)) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (↑f₀ a) ∂↑(μs i))
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
simp_rw [f₀_eq, Function.comp_apply, ENNReal.ofReal_coe_nnreal] at aux auxs
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
f₀_nn : 0 ≤ ↑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ↑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ↑f₀
aux : (∫ (a : Ω), ↑(↑f a) ∂↑μ) = ENNReal.toReal (∫⁻ (a : Ω), ↑(↑f a) ∂↑μ)
auxs : ∀ (i : γ), (∫ (a : Ω), ↑(↑f a) ∂↑(μs i)) = ENNReal.toReal (∫⁻ (a : Ω), ↑(↑f a) ∂↑(μs i))
⊢ Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ)))
simpa only [← aux, ← auxs] using h f₀
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
⊢ ↑f₀ = NNReal.toReal ∘ ↑f
rfl
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
key :
  Tendsto (fun n => ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs n))) F (𝓝 (ENNReal.toReal (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))) ↔
    Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ↑f₀ = NNReal.toReal ∘ ↑f
x✝ : Ω
⊢ OfNat.ofNat 0 x✝ ≤ ↑f₀ x✝
simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]