English
If for all bounded f, 0 ≤ f and a liminf bound holds for the integrals with respect to μs_i, then the limit inferior of the integrals is at least the integral with respect to μ.
Русский
Если для всех ограниченных f выполняется неравенство в отношении liminf интегралов по μs_i против μ, то liminf интегралов больше либо равен интегралу по μ.
LaTeX
$$$$\\forall f, \\; 0 \\le f \\Rightarrow \\liminf_i \\int f d\\mu_i \\ge \\int f d\\mu.$$$$
Lean4
theorem tendsto_integral_of_forall_integral_le_liminf_integral {ι : Type*} {L : Filter ι} {μ : Measure X}
[IsProbabilityMeasure μ] {μs : ι → Measure X} [∀ i, IsProbabilityMeasure (μs i)]
(h : ∀ f : X →ᵇ ℝ, 0 ≤ f → ∫ x, f x ∂μ ≤ L.liminf (fun i ↦ ∫ x, f x ∂(μs i))) (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 ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)
· 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 := liminf_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
rwa [this, add_le_add_iff_right] at key
· 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 := liminf_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
rwa [this, sub_le_sub_iff_left] at key
· exact bdd_above
· exact bdd_below
