English
If E0 ⊆ E ⊆ E1 with μ(E1\\E0) = 0 and μ(E0) ≤ L.liminf μ_s(i,E0) and L.limsup μ_s(i,E1) ≤ μ(E1), then μ_s(i,E) → μ(E).
Русский
Пусть E0 ⊆ E ⊆ E1, μ(E1\\E0)=0 и μ(E0) ≤ liminf μ_s(i,E0) и limsup μ_s(i,E1) ≤ μ(E1). Тогда μ_s(i,E) стремится к μ(E).
LaTeX
$$$\\mathrm{If}\; E_0 \\subseteq E \\subseteq E_1,\; \\mu(E_1\\E_0) = 0,\;\\mu(E_0) \\le L.liminf_i \\mu_s(i,E_0)$ and $L.limsup_i \\mu_s(i,E_1) \\le \\mu(E_1)$, then $L.Tendsto \\mu_s(i,E) (\\mathcal{N}(\\mu(E)))$.$$
Lean4
theorem tendsto_measure_of_le_liminf_measure_of_limsup_measure_le {ι : Type*} {L : Filter ι} {μ : Measure Ω}
{μs : ι → Measure Ω} {E₀ E E₁ : Set Ω} (E₀_subset : E₀ ⊆ E) (subset_E₁ : E ⊆ E₁) (nulldiff : μ (E₁ \ E₀) = 0)
(h_E₀ : μ E₀ ≤ L.liminf fun i ↦ μs i E₀) (h_E₁ : (L.limsup fun i ↦ μs i E₁) ≤ μ E₁) :
L.Tendsto (fun i ↦ μs i E) (𝓝 (μ E)) :=
by
apply tendsto_of_le_liminf_of_limsup_le
· have E₀_ae_eq_E : E₀ =ᵐ[μ] E :=
EventuallyLE.antisymm E₀_subset.eventuallyLE (subset_E₁.eventuallyLE.trans (ae_le_set.mpr nulldiff))
calc
μ E = μ E₀ := measure_congr E₀_ae_eq_E.symm
_ ≤ L.liminf fun i ↦ μs i E₀ := h_E₀
_ ≤ L.liminf fun i ↦ μs i E := liminf_le_liminf (.of_forall fun _ ↦ measure_mono E₀_subset)
· have E_ae_eq_E₁ : E =ᵐ[μ] E₁ :=
EventuallyLE.antisymm subset_E₁.eventuallyLE ((ae_le_set.mpr nulldiff).trans E₀_subset.eventuallyLE)
calc
(L.limsup fun i ↦ μs i E) ≤ L.limsup fun i ↦ μs i E₁ :=
limsup_le_limsup (.of_forall fun _ ↦ measure_mono subset_E₁)
_ ≤ μ E₁ := h_E₁
_ = μ E := measure_congr E_ae_eq_E₁.symm
· infer_param
· infer_param
