English
There is a duality formula: the essSup equals the sInf of a certain set of thresholds, providing a representation via zero-measure sides.
Русский
Существует двойственная формула: essSup равен sInf некоторого множества порогов (нулевая мера слева).
LaTeX
$$$\operatorname{essSup} f μ = sInf \{ a \mid μ\{ x \mid f(x) > a \} = 0 \}$.$$
Lean4
theorem measure_iUnionNotConvergentSeq (hε : 0 < ε) (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g)
(hsm : MeasurableSet s) (hs : μ s ≠ ∞) (hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
μ (iUnionNotConvergentSeq hε hf hg hsm hs hfg) ≤ ENNReal.ofReal ε :=
by
refine
le_trans (measure_iUnion_le _)
(le_trans (ENNReal.tsum_le_tsum <| notConvergentSeqLTIndex_spec (half_pos hε) hf hg hsm hs hfg) ?_)
simp_rw [ENNReal.ofReal_mul (half_pos hε).le]
rw [ENNReal.tsum_mul_left, ← ENNReal.ofReal_tsum_of_nonneg, inv_eq_one_div, tsum_geometric_two, ←
ENNReal.ofReal_mul (half_pos hε).le, div_mul_cancel₀ ε two_ne_zero]
· intro n; positivity
· rw [inv_eq_one_div]
exact summable_geometric_two
