mathlibdocumentation

measure_theory.function.ess_sup

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 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 #

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_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_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (c : β) (hμ : μ 0) :
ess_sup (λ (x : α), c) μ = c
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 ess_inf_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (c : β) (hμ : μ 0) :
ess_inf (λ (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μν : ν μ) :
ν μ
theorem ess_inf_antitone_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} {f : α → β} (hμν : μ ν) :
ν μ
theorem ess_sup_smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {c : ℝ≥0∞} (hc : c 0) :
(c μ) = μ
theorem ae_lt_of_ess_sup_lt {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {x : β} (hf : μ < x) :
∀ᵐ (y : α) ∂μ, f y < x
theorem ae_lt_of_lt_ess_inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {x : β} (hf : x < μ) :
∀ᵐ (y : α) ∂μ, x < f y
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 : α → ℝ≥0∞) :
∀ᵐ (y : α) ∂μ, f y μ
@[simp]
theorem ennreal.ess_sup_eq_zero_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} :
μ = 0 f =ᵐ[μ] 0
theorem ennreal.ess_sup_const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} {a : ℝ≥0∞} :
ess_sup (λ (x : α), a * f x) μ = a * μ
theorem ennreal.ess_sup_add_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α → ℝ≥0∞) :
ess_sup (f + g) μ μ + μ
theorem ennreal.ess_sup_liminf_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] [linear_order ι] (f : ι → α → ℝ≥0∞) :
ess_sup (λ (x : α), filter.at_top.liminf (λ (n : ι), f n x)) μ filter.at_top.liminf (λ (n : ι), ess_sup (λ (x : α), f n x) μ)