mathlib3 documentation

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 #

def ess_sup {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice β] {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} [conditionally_complete_lattice β] {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 α} [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} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_lattice β] {f g : α β} (hfg : f =ᵐ[μ] g) :
ess_inf f μ = ess_inf g μ
@[simp]
theorem ess_sup_const' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_lattice β] [μ.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 α} [conditionally_complete_lattice β] [μ.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 α} [conditionally_complete_lattice β] (c : β) (hμ : μ 0) :
ess_sup (λ (x : α), c) μ = c
theorem ess_inf_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_lattice β] (c : β) (hμ : μ 0) :
ess_inf (λ (x : α), c) μ = c
theorem ess_sup_eq_Inf {α : Type u_1} {β : Type u_2} [conditionally_complete_linear_order β] {m : measurable_space α} (μ : measure_theory.measure α) (f : α β) :
ess_sup f μ = has_Inf.Inf {a : β | μ {x : α | a < f x} = 0}
theorem ess_inf_eq_Sup {α : Type u_1} {β : Type u_2} [conditionally_complete_linear_order β] {m : measurable_space α} (μ : measure_theory.measure α) (f : α β) :
ess_inf 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 α} [conditionally_complete_linear_order β] {x : β} {f : α β} (hx : ess_sup f μ < x) (hf : filter.is_bounded_under has_le.le μ.ae f . "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 α} [conditionally_complete_linear_order β] {x : β} {f : α β} (hx : x < ess_inf f μ) (hf : filter.is_bounded_under ge μ.ae f . "is_bounded_default") :
∀ᵐ (y : α) μ, x < f y
theorem ae_le_ess_sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_linear_order β] {f : α β} [topological_space β] [topological_space.first_countable_topology β] [order_topology β] (hf : filter.is_bounded_under has_le.le μ.ae f . "is_bounded_default") :
∀ᵐ (y : α) μ, f y ess_sup f μ
theorem ae_ess_inf_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_linear_order β] {f : α β} [topological_space β] [topological_space.first_countable_topology β] [order_topology β] (hf : filter.is_bounded_under ge μ.ae f . "is_bounded_default") :
∀ᵐ (y : α) μ, ess_inf f μ f y
theorem meas_ess_sup_lt {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_linear_order β] {f : α β} [topological_space β] [topological_space.first_countable_topology β] [order_topology β] (hf : filter.is_bounded_under has_le.le μ.ae f . "is_bounded_default") :
μ {y : α | ess_sup f μ < f y} = 0
theorem meas_lt_ess_inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [conditionally_complete_linear_order β] {f : α β} [topological_space β] [topological_space.first_countable_topology β] [order_topology β] (hf : filter.is_bounded_under ge μ.ae f . "is_bounded_default") :
μ {y : α | f y < ess_inf f μ} = 0
@[simp]
theorem ess_sup_measure_zero {α : Type u_1} {β : Type u_2} [complete_lattice β] {m : measurable_space α} {f : α β} :
@[simp]
theorem ess_inf_measure_zero {α : Type u_1} {β : Type u_2} [complete_lattice β] {m : measurable_space α} {f : α β} :
theorem ess_sup_mono_ae {α : Type u_1} {β : Type u_2} {m : 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} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] {f g : α β} (hfg : f ≤ᵐ[μ] g) :
ess_inf f μ ess_inf g μ
theorem ess_sup_le_of_ae_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] {f : α β} (c : β) (hf : f ≤ᵐ[μ] λ (_x : α), c) :
ess_sup f μ c
theorem le_ess_inf_of_ae_le {α : Type u_1} {β : Type u_2} {m : 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} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] :
ess_sup (λ (x : α), ) μ =
theorem ess_inf_const_top {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] :
ess_inf (λ (x : α), ) μ =
theorem order_iso.ess_sup_apply {α : Type u_1} {β : Type u_2} [complete_lattice β] {m : measurable_space α} {γ : 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} [complete_lattice β] {m : measurable_space α} {γ : 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} {m : measurable_space α} {μ ν : measure_theory.measure α} [complete_lattice β] {f : α β} (hμν : ν.absolutely_continuous μ) :
ess_sup f ν ess_sup f μ
theorem ess_sup_mono_measure' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [complete_lattice β] {f : α β} (hμν : ν μ) :
ess_sup f ν ess_sup f μ
theorem ess_inf_antitone_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [complete_lattice β] {f : α β} (hμν : μ.absolutely_continuous ν) :
ess_inf f ν ess_inf f μ
theorem ess_sup_smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] {f : α β} {c : ennreal} (hc : c 0) :
ess_sup f (c μ) = ess_sup f μ
theorem ess_sup_comp_le_ess_sup_map_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] {γ : Type u_3} {mγ : measurable_space γ} {f : α γ} {g : γ β} (hf : ae_measurable f μ) :
theorem measurable_embedding.ess_sup_map_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [complete_lattice β] {γ : Type u_3} {mγ : measurable_space γ} {f : α γ} {g : γ β} (hf : measurable_embedding f) :
theorem ess_sup_indicator_eq_ess_sup_restrict {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [complete_linear_order β] [has_zero β] {s : set α} {f : α β} (hf : 0 ≤ᵐ[μ.restrict s] f) (hs : measurable_set s) (hs_not_null : μ s 0) :
ess_sup (s.indicator f) μ = ess_sup f (μ.restrict s)
theorem ennreal.ae_le_ess_sup {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α ennreal) :
∀ᵐ (y : α) μ, f y ess_sup f μ
@[simp]
theorem ennreal.ess_sup_eq_zero_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} :
ess_sup f μ = 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 * ess_sup f μ
theorem ennreal.ess_sup_mul_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α ennreal) :
ess_sup (f * g) μ ess_sup f μ * ess_sup g μ
theorem ennreal.ess_sup_add_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f g : α ennreal) :
ess_sup (f + g) μ ess_sup f μ + ess_sup g μ
theorem ennreal.ess_sup_liminf_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} [countable ι] [linear_order ι] (f : ι α ennreal) :
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 : filter.is_bounded_under has_le.le μ.ae f) :
(ess_sup f μ) = ess_sup (λ (x : α), (f x)) μ