mathlib documentation

measure_theory.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} [measurable_space α] [conditionally_complete_lattice β] (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} [measurable_space α] [conditionally_complete_lattice β] (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} [measurable_space α] {μ : measure_theory.measure α} [conditionally_complete_lattice β] {f g : α → β} (hfg : f =ᵐ[μ] g) :
ess_sup f μ = ess_sup g μ
theorem ess_inf_congr_ae {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [conditionally_complete_lattice β] {f g : α → β} (hfg : f =ᵐ[μ] g) :
ess_inf f μ = ess_inf g μ
@[simp]
theorem ess_sup_measure_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [complete_lattice β] {f : α → β} :
@[simp]
theorem ess_inf_measure_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [complete_lattice β] {f : α → β} :
theorem ess_sup_mono_ae {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] {f g : α → β} (hfg : f ≤ᵐ[μ] g) :
ess_sup f μ ess_sup g μ
theorem ess_inf_mono_ae {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] {f g : α → β} (hfg : f ≤ᵐ[μ] g) :
ess_inf f μ ess_inf g μ
theorem ess_sup_const {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] (c : β) (hμ : μ 0) :
ess_sup (λ (x : α), c) μ = c
theorem ess_sup_le_of_ae_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] {f : α → β} (c : β) (hf : f ≤ᵐ[μ] λ (_x : α), c) :
ess_sup f μ c
theorem ess_inf_const {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] (c : β) (hμ : μ 0) :
ess_inf (λ (x : α), c) μ = c
theorem le_ess_inf_of_ae_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] {f : α → β} (c : β) (hf : (λ (_x : α), c) ≤ᵐ[μ] f) :
c ess_inf f μ
theorem ess_sup_const_bot {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] :
ess_sup (λ (x : α), ) μ =
theorem ess_inf_const_top {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] :
ess_inf (λ (x : α), ) μ =
theorem order_iso.ess_sup_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [complete_lattice β] {γ : Type u_3} [complete_lattice γ] (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} [measurable_space α] [complete_lattice β] {γ : Type u_3} [complete_lattice γ] (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} [measurable_space α] [complete_lattice β] {f : α → β} {μ ν : measure_theory.measure α} (hμν : ν μ) :
ess_sup f ν ess_sup f μ
theorem ess_inf_antimono_measure {α : Type u_1} {β : Type u_2} [measurable_space α] [complete_lattice β] {f : α → β} {μ ν : measure_theory.measure α} (hμν : μ ν) :
ess_inf f ν ess_inf f μ
theorem ae_lt_of_ess_sup_lt {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_linear_order β] {f : α → β} {x : β} (hf : ess_sup f μ < x) :
∀ᵐ (y : α) ∂μ, f y < x
theorem ae_lt_of_lt_ess_inf {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_linear_order β] {f : α → β} {x : β} (hf : x < ess_inf f μ) :
∀ᵐ (y : α) ∂μ, x < f y
theorem ennreal.ae_le_ess_sup {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α → ℝ≥0∞) :
∀ᵐ (y : α) ∂μ, f y ess_sup f μ
@[simp]
theorem ennreal.ess_sup_eq_zero_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → ℝ≥0∞} :
ess_sup f μ = 0 f =ᵐ[μ] 0
theorem ennreal.ess_sup_const_mul {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → ℝ≥0∞} {a : ℝ≥0∞} :
ess_sup (λ (x : α), a * f x) μ = a * ess_sup f μ
theorem ennreal.ess_sup_add_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f g : α → ℝ≥0∞) :
ess_sup (f + g) μ ess_sup f μ + ess_sup g μ
theorem ennreal.ess_sup_liminf_le {α : Type u_1} [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) μ)