English
If for all measurable E with μ(frontier E)=0, the measures μ_s(i)(E) converge to μ(E), then for all closed F we have limsup μ_s(i)(F) ≤ μ(F).
Русский
Если для всех измеримых E с μ(frontier E)=0 меры μ_s(i)(E) сходятся к μ(E), то для всех замкнутых F выполняется limsup μ_s(i)(F) ≤ μ(F).
LaTeX
$$$\bigl(\forall E,\; \text{Measurable}(E) \land μ(\text{frontier}(E)) = 0 \Rightarrow Tendsto (i\mapsto μ_s(i,E)) L (\mathcal{N}(μ(E)))\bigr) \Rightarrow \forall F,\; F\text{ closed} \Rightarrow L.limsup (i\mapsto μ_s(i,F)) ≤ μ(F)$$$
Lean4
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all closed sets F we have the limsup condition limsup μsᵢ(F) ≤ μ(F). -/
theorem limsup_measure_closed_le_of_forall_tendsto_measure {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω]
[TopologicalSpace Ω] [PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
{μs : ι → Measure Ω}
(h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ μs i E) L (𝓝 (μ E))) (F : Set Ω)
(F_closed : IsClosed F) : L.limsup (fun i ↦ μs i F) ≤ μ F :=
by
letI : PseudoMetricSpace Ω := TopologicalSpace.pseudoMetrizableSpacePseudoMetric Ω
rcases L.eq_or_neBot with rfl | _
· simp only [limsup_bot, bot_eq_zero', zero_le]
have ex := exists_null_frontiers_thickening μ F
let rs := Classical.choose ex
have rs_lim : Tendsto rs atTop (𝓝 0) := (Classical.choose_spec ex).1
have rs_pos : ∀ n, 0 < rs n := fun n ↦ ((Classical.choose_spec ex).2 n).1
have rs_null : ∀ n, μ (frontier (Metric.thickening (rs n) F)) = 0 := fun n ↦ ((Classical.choose_spec ex).2 n).2
have Fthicks_open : ∀ n, IsOpen (Metric.thickening (rs n) F) := fun n ↦ Metric.isOpen_thickening
have key := fun (n : ℕ) ↦ h (Fthicks_open n).measurableSet (rs_null n)
apply ENNReal.le_of_forall_pos_le_add
intro ε ε_pos μF_finite
have keyB :=
tendsto_measure_cthickening_of_isClosed (μ := μ) (s := F)
⟨1, ⟨by simp only [gt_iff_lt, zero_lt_one], measure_ne_top _ _⟩⟩ F_closed
have nhds : Iio (μ F + ε) ∈ 𝓝 (μ F) :=
Iio_mem_nhds <| ENNReal.lt_add_right μF_finite.ne (ENNReal.coe_pos.mpr ε_pos).ne'
specialize rs_lim (keyB nhds)
simp only [mem_map, mem_atTop_sets, ge_iff_le, mem_preimage, mem_Iio] at rs_lim
obtain ⟨m, hm⟩ := rs_lim
have aux : (fun i ↦ (μs i F)) ≤ᶠ[L] (fun i ↦ μs i (Metric.thickening (rs m) F)) :=
.of_forall <| fun i ↦ measure_mono (Metric.self_subset_thickening (rs_pos m) F)
refine (limsup_le_limsup aux).trans ?_
rw [Tendsto.limsup_eq (key m)]
apply (measure_mono (Metric.thickening_subset_cthickening (rs m) F)).trans (hm m rfl.le).le
