# mathlib3documentation

measure_theory.function.ess_sup

# Essential supremum and infimum #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 measure_theory/lp_space.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 measure_theory/ae_eq_fun.lean).

## Main definitions #

• ess_sup f μ := μ.ae.limsup f
• ess_inf f μ := μ.ae.liminf f
def ess_sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} (f : α β) (μ : measure_theory.measure α) :
β

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

Equations
def ess_inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} (f : α β) (μ : measure_theory.measure α) :
β

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

Equations
theorem ess_sup_congr_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α β} (hfg : f =ᵐ[μ] g) :
μ = μ
theorem ess_inf_congr_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α β} (hfg : f =ᵐ[μ] g) :
μ = μ
@[simp]
theorem ess_sup_const' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [μ.ae.ne_bot] (c : β) :
ess_sup (λ (x : α), c) μ = c
@[simp]
theorem ess_inf_const' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [μ.ae.ne_bot] (c : β) :
ess_inf (λ (x : α), c) μ = c
theorem ess_sup_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (c : β) (hμ : μ 0) :
ess_sup (λ (x : α), c) μ = c
theorem ess_inf_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (c : β) (hμ : μ 0) :
ess_inf (λ (x : α), c) μ = c
theorem ess_sup_eq_Inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) (f : α β) :
μ = has_Inf.Inf {a : β | μ {x : α | a < f x} = 0}
theorem ess_inf_eq_Sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) (f : α β) :
μ = has_Sup.Sup {a : β | μ {x : α | f x < a} = 0}
theorem ae_lt_of_ess_sup_lt {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {x : β} {f : α β} (hx : μ < x) (hf : . "is_bounded_default") :
∀ᵐ (y : α) μ, f y < x
theorem ae_lt_of_lt_ess_inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {x : β} {f : α β} (hx : x < μ) (hf : . "is_bounded_default") :
∀ᵐ (y : α) μ, x < f y
theorem ae_le_ess_sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} (hf : . "is_bounded_default") :
∀ᵐ (y : α) μ, f y μ
theorem ae_ess_inf_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} (hf : . "is_bounded_default") :
∀ᵐ (y : α) μ, μ f y
theorem meas_ess_sup_lt {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} (hf : . "is_bounded_default") :
μ {y : α | μ < f y} = 0
theorem meas_lt_ess_inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} (hf : . "is_bounded_default") :
μ {y : α | f y < μ} = 0
@[simp]
theorem ess_sup_measure_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : α β} :
0 =
@[simp]
theorem ess_inf_measure_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : α β} :
0 =
theorem ess_sup_mono_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α β} (hfg : f ≤ᵐ[μ] g) :
μ μ
theorem ess_inf_mono_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α β} (hfg : f ≤ᵐ[μ] g) :
μ μ
theorem ess_sup_le_of_ae_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} (c : β) (hf : f ≤ᵐ[μ] λ (_x : α), c) :
μ c
theorem le_ess_inf_of_ae_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} (c : β) (hf : (λ (_x : α), c) ≤ᵐ[μ] f) :
c μ
theorem ess_sup_const_bot {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α}  :
ess_sup (λ (x : α), ) μ =
theorem ess_inf_const_top {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α}  :
ess_inf (λ (x : α), ) μ =
theorem order_iso.ess_sup_apply {α : Type u_1} {β : Type u_2} {m : measurable_space α} {γ : Type u_3} (f : α β) (μ : measure_theory.measure α) (g : β ≃o γ) :
g (ess_sup f μ) = ess_sup (λ (x : α), g (f x)) μ
theorem order_iso.ess_inf_apply {α : Type u_1} {β : Type u_2} {m : measurable_space α} {γ : Type u_3} (f : α β) (μ : measure_theory.measure α) (g : β ≃o γ) :
g (ess_inf f μ) = ess_inf (λ (x : α), g (f x)) μ
theorem ess_sup_mono_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} {f : α β} (hμν : ν.absolutely_continuous μ) :
ν μ
theorem ess_sup_mono_measure' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} {f : α β} (hμν : ν μ) :
ν μ
theorem ess_inf_antitone_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} {f : α β} (hμν : μ.absolutely_continuous ν) :
ν μ
theorem ess_sup_smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α β} {c : ennreal} (hc : c 0) :
(c μ) = μ
theorem ess_sup_comp_le_ess_sup_map_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {γ : Type u_3} {mγ : measurable_space γ} {f : α γ} {g : γ β} (hf : μ) :
ess_sup (g f) μ
theorem measurable_embedding.ess_sup_map_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {γ : Type u_3} {mγ : measurable_space γ} {f : α γ} {g : γ β} (hf : measurable_embedding f) :
= ess_sup (g f) μ
theorem ess_sup_map_measure_of_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {γ : Type u_3} {mγ : measurable_space γ} {f : α γ} {g : γ β} (hg : measurable g) (hf : μ) :
= ess_sup (g f) μ
theorem ess_sup_map_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {γ : Type u_3} {mγ : measurable_space γ} {f : α γ} {g : γ β} (hg : ) (hf : μ) :
= ess_sup (g f) μ
theorem ess_sup_indicator_eq_ess_sup_restrict {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [has_zero β] {s : set α} {f : α β} (hf : 0 ≤ᵐ[μ.restrict s] f) (hs : measurable_set s) (hs_not_null : μ s 0) :
ess_sup (s.indicator f) μ = (μ.restrict s)
theorem ennreal.ae_le_ess_sup {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) :
∀ᵐ (y : α) μ, f y μ
@[simp]
theorem ennreal.ess_sup_eq_zero_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} :
μ = 0 f =ᵐ[μ] 0
theorem ennreal.ess_sup_const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} {a : ennreal} :
ess_sup (λ (x : α), a * f x) μ = a * μ
theorem ennreal.ess_sup_mul_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α ennreal) :
ess_sup (f * g) μ μ * μ
theorem ennreal.ess_sup_add_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α ennreal) :
ess_sup (f + g) μ μ + μ
theorem ennreal.ess_sup_liminf_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} [countable ι] [linear_order ι] (f : ι ) :
ess_sup (λ (x : α), filter.liminf (λ (n : ι), f n x) filter.at_top) μ filter.liminf (λ (n : ι), ess_sup (λ (x : α), f n x) μ) filter.at_top
theorem ennreal.coe_ess_sup {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α nnreal} (hf : f) :
(ess_sup f μ) = ess_sup (λ (x : α), (f x)) μ