# Documentation

Mathlib.MeasureTheory.Function.EssSup

# Essential supremum and infimum #

We define the essential supremum and infimum of a function f : α → β with respect to a measure μ on α. The essential supremum is the infimum of the constants c : β such that f x ≤ c almost everywhere.

TODO: The essential supremum of functions α → ℝ≥0∞ is used in particular to define the norm in the L∞ space (see MeasureTheory/LpSpace.lean).

There is a different quantity which is sometimes also called essential supremum: the least upper-bound among measurable functions of a family of measurable functions (in an almost-everywhere sense). We do not define that quantity here, which is simply the supremum of a map with values in α →ₘ[μ] β (see MeasureTheory/AEEqFun.lean).

## Main definitions #

• essSup f μ := μ.ae.limsup f
• essInf f μ := μ.ae.liminf f
def essSup {α : Type u_1} {β : Type u_2} :
{x : } → (αβ) →

Essential supremum of f with respect to measure μ: the smallest c : β such that f x ≤ c a.e.

Instances For
def essInf {α : Type u_1} {β : Type u_2} :
{x : } → (αβ) →

Essential infimum of f with respect to measure μ: the greatest c : β such that c ≤ f x a.e.

Instances For
theorem essSup_congr_ae {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} {g : αβ} (hfg : ) :
essSup f μ = essSup g μ
theorem essInf_congr_ae {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} {g : αβ} (hfg : ) :
essInf f μ = essInf g μ
@[simp]
theorem essSup_const' {α : Type u_1} {β : Type u_2} {m : } {μ : } [] (c : β) :
essSup (fun x => c) μ = c
@[simp]
theorem essInf_const' {α : Type u_1} {β : Type u_2} {m : } {μ : } [] (c : β) :
essInf (fun x => c) μ = c
theorem essSup_const {α : Type u_1} {β : Type u_2} {m : } {μ : } (c : β) (hμ : μ 0) :
essSup (fun x => c) μ = c
theorem essInf_const {α : Type u_1} {β : Type u_2} {m : } {μ : } (c : β) (hμ : μ 0) :
essInf (fun x => c) μ = c
theorem essSup_eq_sInf {α : Type u_1} {β : Type u_2} {m : } (μ : ) (f : αβ) :
essSup f μ = sInf {a | μ {x | a < f x} = 0}
theorem essInf_eq_sSup {α : Type u_1} {β : Type u_2} {m : } (μ : ) (f : αβ) :
essInf f μ = sSup {a | μ {x | f x < a} = 0}
theorem ae_lt_of_essSup_lt {α : Type u_1} {β : Type u_2} {m : } {μ : } {x : β} {f : αβ} (hx : essSup f μ < x) (hf : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) _auto✝) :
∀ᵐ (y : α) ∂μ, f y < x
theorem ae_lt_of_lt_essInf {α : Type u_1} {β : Type u_2} {m : } {μ : } {x : β} {f : αβ} (hx : x < essInf f μ) (hf : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) _auto✝) :
∀ᵐ (y : α) ∂μ, x < f y
theorem ae_le_essSup {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} [] [] (hf : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) _auto✝) :
∀ᵐ (y : α) ∂μ, f y essSup f μ
theorem ae_essInf_le {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} [] [] (hf : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) _auto✝) :
∀ᵐ (y : α) ∂μ, essInf f μ f y
theorem meas_essSup_lt {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} [] [] (hf : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) _auto✝) :
μ {y | essSup f μ < f y} = 0
theorem meas_lt_essInf {α : Type u_1} {β : Type u_2} {m : } {μ : } {f : αβ} [] [] (hf : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) _auto✝) :
μ {y | f y < essInf f μ} = 0
@[simp]
theorem essSup_measure_zero {α : Type u_1} {β : Type u_2} [] {m : } {f : αβ} :
@[simp]
theorem essInf_measure_zero {α : Type u_1} {β : Type u_2} [] :
∀ {x : } {f : αβ}, essInf f 0 =
theorem essSup_mono_ae {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : αβ} {g : αβ} (hfg : ) :
essSup f μ essSup g μ
theorem essInf_mono_ae {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : αβ} {g : αβ} (hfg : ) :
essInf f μ essInf g μ
theorem essSup_le_of_ae_le {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : αβ} (c : β) (hf : f ≤ᶠ[] fun x => c) :
essSup f μ c
theorem le_essInf_of_ae_le {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : αβ} (c : β) (hf : (fun x => c) ≤ᶠ[] f) :
c essInf f μ
theorem essSup_const_bot {α : Type u_1} {β : Type u_2} {m : } {μ : } [] :
essSup (fun x => ) μ =
theorem essInf_const_top {α : Type u_1} {β : Type u_2} {m : } {μ : } [] :
essInf (fun x => ) μ =
theorem OrderIso.essSup_apply {α : Type u_1} {β : Type u_2} [] {m : } {γ : Type u_3} [] (f : αβ) (μ : ) (g : β ≃o γ) :
g (essSup f μ) = essSup (fun x => g (f x)) μ
theorem OrderIso.essInf_apply {α : Type u_1} {β : Type u_2} [] :
∀ {x : } {γ : Type u_3} [inst : ] (f : αβ) (μ : ) (g : β ≃o γ), g (essInf f μ) = essInf (fun x => g (f x)) μ
theorem essSup_mono_measure {α : Type u_1} {β : Type u_2} {m : } {μ : } {ν : } [] {f : αβ} (hμν : ) :
essSup f ν essSup f μ
theorem essSup_mono_measure' {α : Type u_3} {β : Type u_4} :
∀ {x : } {μ ν : } [inst : ] {f : αβ}, ν μessSup f ν essSup f μ
theorem essInf_antitone_measure {α : Type u_1} {β : Type u_2} {m : } {μ : } {ν : } [] {f : αβ} (hμν : ) :
essInf f ν essInf f μ
theorem essSup_smul_measure {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {f : αβ} {c : ENNReal} (hc : c 0) :
essSup f (c μ) = essSup f μ
theorem essSup_comp_le_essSup_map_measure {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {γ : Type u_3} {mγ : } {f : αγ} {g : γβ} (hf : ) :
essSup (g f) μ
theorem MeasurableEmbedding.essSup_map_measure {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {γ : Type u_3} {mγ : } {f : αγ} {g : γβ} (hf : ) :
= essSup (g f) μ
theorem essSup_map_measure_of_measurable {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {γ : Type u_3} {mγ : } {f : αγ} {g : γβ} [] [] (hg : ) (hf : ) :
= essSup (g f) μ
theorem essSup_map_measure {α : Type u_1} {β : Type u_2} {m : } {μ : } [] {γ : Type u_3} {mγ : } {f : αγ} {g : γβ} [] [] (hg : ) (hf : ) :
= essSup (g f) μ
theorem essSup_indicator_eq_essSup_restrict {α : Type u_1} {β : Type u_2} {m : } {μ : } [Zero β] {s : Set α} {f : αβ} (hf : ) (hs : ) (hs_not_null : μ s 0) :
essSup () μ =
theorem ENNReal.ae_le_essSup {α : Type u_1} {m : } {μ : } (f : αENNReal) :
∀ᵐ (y : α) ∂μ, f y essSup f μ
@[simp]
theorem ENNReal.essSup_eq_zero_iff {α : Type u_1} {m : } {μ : } {f : αENNReal} :
essSup f μ = 0
theorem ENNReal.essSup_const_mul {α : Type u_1} {m : } {μ : } {f : αENNReal} {a : ENNReal} :
essSup (fun x => a * f x) μ = a * essSup f μ
theorem ENNReal.essSup_mul_le {α : Type u_1} {m : } {μ : } (f : αENNReal) (g : αENNReal) :
essSup (f * g) μ essSup f μ * essSup g μ
theorem ENNReal.essSup_add_le {α : Type u_1} {m : } {μ : } (f : αENNReal) (g : αENNReal) :
essSup (f + g) μ essSup f μ + essSup g μ
theorem ENNReal.essSup_liminf_le {α : Type u_1} {m : } {μ : } {ι : Type u_3} [] [] (f : ιαENNReal) :
essSup (fun x => Filter.liminf (fun n => f n x) Filter.atTop) μ Filter.liminf (fun n => essSup (fun x => f n x) μ) Filter.atTop
theorem ENNReal.coe_essSup {α : Type u_1} {m : } {μ : } {f : αNNReal} (hf : Filter.IsBoundedUnder (fun x x_1 => x x_1) () f) :
↑(essSup f μ) = essSup (fun x => ↑(f x)) μ