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 constantsc : βsuch thatf x ≤ calmost 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
- ess_sup f μ = filter.limsup f μ.ae
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
- ess_inf f μ = filter.liminf f μ.ae
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) :
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) :
@[simp]
theorem
ess_sup_const'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[conditionally_complete_lattice β]
[μ.ae.ne_bot]
(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 : β) :
theorem
ess_sup_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[conditionally_complete_lattice β]
(c : β)
(hμ : μ ≠ 0) :
theorem
ess_inf_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[conditionally_complete_lattice β]
(c : β)
(hμ : μ ≠ 0) :
theorem
ess_sup_eq_Inf
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order β]
{m : measurable_space α}
(μ : measure_theory.measure α)
(f : α → β) :
theorem
ess_inf_eq_Sup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order β]
{m : measurable_space α}
(μ : measure_theory.measure α)
(f : α → β) :
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") :
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") :
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") :
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") :
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") :
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") :
@[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) :
theorem
ess_inf_mono_ae
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[complete_lattice β]
{f g : α → β}
(hfg : f ≤ᵐ[μ] 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) :
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) :
theorem
ess_sup_const_bot
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[complete_lattice β] :
theorem
ess_inf_const_top
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[complete_lattice β] :
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 γ) :
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 γ) :
theorem
ess_sup_mono_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[complete_lattice β]
{f : α → β}
(hμν : ν.absolutely_continuous μ) :
theorem
ess_sup_mono_measure'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[complete_lattice β]
{f : α → β}
(hμν : ν ≤ μ) :
theorem
ess_inf_antitone_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[complete_lattice β]
{f : α → β}
(hμν : μ.absolutely_continuous ν) :
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) :
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 μ) :
ess_sup (g ∘ f) μ ≤ ess_sup g (measure_theory.measure.map 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) :
ess_sup g (measure_theory.measure.map f μ) = ess_sup (g ∘ f) μ
theorem
ess_sup_map_measure_of_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[complete_lattice β]
{γ : Type u_3}
{mγ : measurable_space γ}
{f : α → γ}
{g : γ → β}
[measurable_space β]
[topological_space β]
[topological_space.second_countable_topology β]
[order_closed_topology β]
[opens_measurable_space β]
(hg : measurable g)
(hf : ae_measurable f μ) :
ess_sup g (measure_theory.measure.map f μ) = ess_sup (g ∘ f) μ
theorem
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 : γ → β}
[measurable_space β]
[topological_space β]
[topological_space.second_countable_topology β]
[order_closed_topology β]
[opens_measurable_space β]
(hg : ae_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
ess_sup g (measure_theory.measure.map f μ) = ess_sup (g ∘ 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) :
theorem
ennreal.ae_le_ess_sup
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ennreal) :
@[simp]
theorem
ennreal.ess_sup_eq_zero_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal} :
theorem
ennreal.ess_sup_const_mul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal}
{a : ennreal} :
theorem
ennreal.ess_sup_mul_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f g : α → ennreal) :
theorem
ennreal.ess_sup_add_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(f g : α → ennreal) :
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) :