English
Let f: α → ℝ≥0, which is bounded a.e. from above. Then the essential supremum computed in NNReal, when viewed as ENNReal, equals the ENNReal essential supremum of f considered as ENNReal-valued:
Русский
Пусть f: α → ℝ≥0 и неравномерно ограничено сверху почти всюду. Тогда essSup f μ, рассматриванное как ENNReal, равно essSup, взятому над f как ENNReal.
LaTeX
$$$$ \bigl( \operatorname{ess\,sup}_{\mu} f \bigr) : \mathbb{R}_{\ge 0} \; = \; \operatorname{ess\,sup}_{x} (f(x) : \mathbb{R}_{\ge 0∞}) µ $$$$
Lean4
theorem coe_essSup {f : α → ℝ≥0} (hf : IsBoundedUnder (· ≤ ·) (ae μ) f) :
((essSup f μ : ℝ≥0) : ℝ≥0∞) = essSup (fun x => (f x : ℝ≥0∞)) μ :=
(ENNReal.coe_sInf <| hf).trans <|
eq_of_forall_le_iff fun r => by simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]; rfl
