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 #

ess_sup f μ := μ.ae.limsup f
ess_inf f μ := μ.ae.liminf f

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

ess_sup f μ = μ.ae.limsup f

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

ess_inf f μ = μ.ae.liminf f

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 : α → β} :

ess_sup f 0 = ⊥

@[simp]

theorem ess_inf_measure_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [complete_lattice β] {f : α → β} :

ess_inf f 0 = ⊤

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_inf_const {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [complete_lattice β] (c : β) (hμ : μ ≠ 0) :

ess_inf (λ (x : α), c) μ = c

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 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) μ)