English
As n tends to infinity, the sequence n ↦ ν(μ.sigmaFiniteSetGE(ν, n)) converges to the supremum of ν(s) over all measurable s with μ|s sigma-finite.
Русский
По мере увелечения n последовательность ν(μ.sigmaFiniteSetGE(ν, n)) сходится к супремуму ν(s) по всем измеримым s, для которых μ|s сигма-финитна.
LaTeX
$$$$\lim_{n\to\infty} \nu\left(\mu\sigmaFiniteSetGE(\nu, n)\right) = \sup_{s:\text{MeasurableSet},\ \SigmaFinite(\mu\restriction s)} \nu(s).$$$$
Lean4
theorem tendsto_measure_sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] :
Tendsto (fun n ↦ ν (μ.sigmaFiniteSetGE ν n)) atTop
(𝓝 (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)) :=
by
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds (measure_sigmaFiniteSetGE_ge μ ν)
(measure_sigmaFiniteSetGE_le μ ν)
nth_rewrite 2 [← tsub_zero (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)]
refine ENNReal.Tendsto.sub tendsto_const_nhds ?_ (Or.inr ENNReal.zero_ne_top)
simp only [one_div]
exact ENNReal.tendsto_inv_nat_nhds_zero
