English
For a sequence of finite measures μ_s(i) converging to μ, the limsup of μ_s(i,F) for any closed F is at most μ(F).
Русский
Для последовательности конечных мер μ_s(i), сходящейся к μ, для любого замкнутого F выполняется limsup μ_s(i,F) ≤ μ(F).
LaTeX
$$$\text{If } μ_s \to μ,\; F\text{ closed} \Rightarrow \limsup_i (μ_s(i)(F)) \le μ(F)$$$
Lean4
/-- One implication of the portmanteau theorem:
Weak convergence of finite measures implies that the limsup of the measures of any closed set is
at most the measure of the closed set under the limit measure.
-/
theorem limsup_measure_closed_le_of_tendsto {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω]
[HasOuterApproxClosed Ω] [OpensMeasurableSpace Ω] {μ : FiniteMeasure Ω} {μs : ι → FiniteMeasure Ω}
(μs_lim : Tendsto μs L (𝓝 μ)) {F : Set Ω} (F_closed : IsClosed F) :
(L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F :=
by
rcases L.eq_or_neBot with rfl | hne
· simp only [limsup_bot, bot_le]
apply ENNReal.le_of_forall_pos_le_add
intro ε ε_pos _
have ε_pos' := (ENNReal.half_pos (ENNReal.coe_ne_zero.mpr ε_pos.ne.symm)).ne.symm
let fs := F_closed.apprSeq
have key₁ : Tendsto (fun n ↦ ∫⁻ ω, (fs n ω : ℝ≥0∞) ∂μ) atTop (𝓝 ((μ : Measure Ω) F)) :=
HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed (μ : Measure Ω)
have room₁ : (μ : Measure Ω) F < (μ : Measure Ω) F + ε / 2 :=
ENNReal.lt_add_right (measure_lt_top (μ : Measure Ω) F).ne ε_pos'
obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁
have key₂ := FiniteMeasure.tendsto_iff_forall_lintegral_tendsto.mp μs_lim (fs M)
have room₂ : (lintegral (μ : Measure Ω) fun a ↦ fs M a) < (lintegral (μ : Measure Ω) fun a ↦ fs M a) + ε / 2 :=
ENNReal.lt_add_right (ne_of_lt ((fs M).lintegral_lt_top_of_nnreal _)) ε_pos'
have ev_near := key₂.eventually_le_const room₂
have ev_near' := ev_near.mono (fun n ↦ le_trans (HasOuterApproxClosed.measure_le_lintegral F_closed (μs n) M))
apply (Filter.limsup_le_limsup ev_near').trans
rw [limsup_const]
apply le_trans (add_le_add (hM M rfl.le).le (le_refl (ε / 2 : ℝ≥0∞)))
simp only [add_assoc, ENNReal.add_halves, le_refl]
