English
If a family of probability measures μs_i yields limsup of integrals bounded above by the integral with respect to μ for all bounded real-valued functions f, then the corresponding integrals converge along L to the integral with respect to μ.
Русский
Если семейство мер μs_i выписывает limsup интегралов выше ограниченного функционирования как в интеграле по μ, то интегралы сходятся по L к интегралу по μ.
LaTeX
$$$$\\text{Tendsto}\\left(i \\mapsto \\int f, d\\mu_i\\right)_{i\\to L} \\to \\int f d\\mu.$$$$
Lean4
theorem tendsto_integral_of_forall_limsup_integral_le_integral {ι : Type*} {L : Filter ι} {μ : Measure X}
[IsProbabilityMeasure μ] {μs : ι → Measure X} [∀ i, IsProbabilityMeasure (μs i)]
(h : ∀ f : X →ᵇ ℝ, 0 ≤ f → L.limsup (fun i ↦ ∫ x, f x ∂(μs i)) ≤ ∫ x, f x ∂μ) (f : X →ᵇ ℝ) :
Tendsto (fun i ↦ ∫ x, f x ∂(μs i)) L (𝓝 (∫ x, f x ∂μ)) :=
by
rcases eq_or_neBot L with rfl | hL
· simp only [tendsto_bot]
have obs := BoundedContinuousFunction.isBounded_range_integral μs f
have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)
have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)
apply tendsto_of_le_liminf_of_limsup_le _ _ bdd_above bdd_below
· have key := h _ (f.norm_sub_nonneg)
simp_rw [f.integral_const_sub ‖f‖] at key
simp only [measureReal_univ_eq_one, smul_eq_mul, one_mul] at key
have := limsup_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
rwa [this, _root_.sub_le_sub_iff_left ‖f‖] at key
· have key := h _ (f.add_norm_nonneg)
simp_rw [f.integral_add_const ‖f‖] at key
simp only [measureReal_univ_eq_one, smul_eq_mul, one_mul] at key
have := limsup_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
rwa [this, add_le_add_iff_right] at key
