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 Mathlib.MeasureTheory.Function.LpSpace).
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 Mathlib.MeasureTheory.Function.AEEqFun).
Main definitions #
def
essSup
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice β]
:
{x : MeasurableSpace α} → (α → β) → MeasureTheory.Measure α → β
Essential supremum of f with respect to measure μ: the smallest c : β such that
f x ≤ c a.e.
Equations
- essSup f μ = Filter.limsup f (MeasureTheory.ae μ)
Instances For
def
essInf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice β]
:
{x : MeasurableSpace α} → (α → β) → MeasureTheory.Measure α → β
Essential infimum of f with respect to measure μ: the greatest c : β such that
c ≤ f x a.e.
Equations
- essInf f μ = Filter.liminf f (MeasureTheory.ae μ)
Instances For
theorem
essSup_congr_ae
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
{f : α → β}
{g : α → β}
(hfg : f =ᵐ[μ] g)
:
theorem
essInf_congr_ae
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
{f : α → β}
{g : α → β}
(hfg : f =ᵐ[μ] g)
:
@[simp]
theorem
essSup_const'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
[NeZero μ]
(c : β)
:
@[simp]
theorem
essInf_const'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
[NeZero μ]
(c : β)
:
theorem
essSup_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
(c : β)
(hμ : μ ≠ 0)
:
theorem
essInf_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
(c : β)
(hμ : μ ≠ 0)
:
@[simp]
theorem
essSup_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
{R : Type u_3}
[Zero R]
[SMulWithZero R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[NoZeroSMulDivisors R ENNReal]
{c : R}
(hc : c ≠ 0)
(f : α → β)
:
theorem
essSup_eq_ciSup
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
{f : α → β}
[Nonempty α]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(hf : BddAbove (Set.range f))
:
theorem
essInf_eq_ciInf
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLattice β]
{f : α → β}
[Nonempty α]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(hf : BddBelow (Set.range f))
:
@[simp]
theorem
essSup_count_eq_ciSup
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[ConditionallyCompleteLattice β]
{f : α → β}
[Nonempty α]
[MeasurableSingletonClass α]
(hf : BddAbove (Set.range f))
:
@[simp]
theorem
essInf_count_eq_ciInf
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[ConditionallyCompleteLattice β]
{f : α → β}
[Nonempty α]
[MeasurableSingletonClass α]
(hf : BddBelow (Set.range f))
:
@[simp]
theorem
essSup_uniformOn_eq_ciSup
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[ConditionallyCompleteLattice β]
{f : α → β}
[Nonempty α]
[MeasurableSingletonClass α]
[Finite α]
(hf : BddAbove (Set.range f))
:
essSup f (ProbabilityTheory.uniformOn Set.univ) = ⨆ (a : α), f a
@[simp]
theorem
essInf_cond_count_eq_ciInf
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[ConditionallyCompleteLattice β]
{f : α → β}
[Nonempty α]
[MeasurableSingletonClass α]
[Finite α]
(hf : BddBelow (Set.range f))
:
essInf f (ProbabilityTheory.uniformOn Set.univ) = ⨅ (a : α), f a
theorem
essSup_eq_sInf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder β]
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(f : α → β)
:
theorem
essInf_eq_sSup
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder β]
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(f : α → β)
:
theorem
ae_lt_of_essSup_lt
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLinearOrder β]
{x : β}
{f : α → β}
(hx : essSup f μ < x)
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) (MeasureTheory.ae μ) f) _auto✝)
:
∀ᵐ (y : α) ∂μ, f y < x
theorem
ae_lt_of_lt_essInf
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLinearOrder β]
{x : β}
{f : α → β}
(hx : x < essInf f μ)
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) (MeasureTheory.ae μ) f) _auto✝)
:
∀ᵐ (y : α) ∂μ, x < f y
theorem
ae_le_essSup
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLinearOrder β]
{f : α → β}
[TopologicalSpace β]
[FirstCountableTopology β]
[OrderTopology β]
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) (MeasureTheory.ae μ) f) _auto✝)
:
theorem
ae_essInf_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLinearOrder β]
{f : α → β}
[TopologicalSpace β]
[FirstCountableTopology β]
[OrderTopology β]
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) (MeasureTheory.ae μ) f) _auto✝)
:
theorem
meas_essSup_lt
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLinearOrder β]
{f : α → β}
[TopologicalSpace β]
[FirstCountableTopology β]
[OrderTopology β]
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) (MeasureTheory.ae μ) f) _auto✝)
:
theorem
meas_lt_essInf
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[ConditionallyCompleteLinearOrder β]
{f : α → β}
[TopologicalSpace β]
[FirstCountableTopology β]
[OrderTopology β]
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) (MeasureTheory.ae μ) f) _auto✝)
:
@[simp]
theorem
essSup_measure_zero
{α : Type u_1}
{β : Type u_2}
[CompleteLattice β]
{m : MeasurableSpace α}
{f : α → β}
:
@[simp]
theorem
essInf_measure_zero
{α : Type u_1}
{β : Type u_2}
[CompleteLattice β]
:
∀ {x : MeasurableSpace α} {f : α → β}, essInf f 0 = ⊤
theorem
essSup_mono_ae
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{f : α → β}
{g : α → β}
(hfg : f ≤ᵐ[μ] g)
:
theorem
essInf_mono_ae
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{f : α → β}
{g : α → β}
(hfg : f ≤ᵐ[μ] g)
:
theorem
essSup_le_of_ae_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{f : α → β}
(c : β)
(hf : f ≤ᵐ[μ] fun (x : α) => c)
:
theorem
le_essInf_of_ae_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{f : α → β}
(c : β)
(hf : (fun (x : α) => c) ≤ᵐ[μ] f)
:
theorem
essSup_const_bot
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
:
theorem
essInf_const_top
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
:
theorem
OrderIso.essSup_apply
{α : Type u_1}
{β : Type u_2}
[CompleteLattice β]
{m : MeasurableSpace α}
{γ : Type u_3}
[CompleteLattice γ]
(f : α → β)
(μ : MeasureTheory.Measure α)
(g : β ≃o γ)
:
theorem
OrderIso.essInf_apply
{α : Type u_1}
{β : Type u_2}
[CompleteLattice β]
:
∀ {x : MeasurableSpace α} {γ : Type u_3} [inst : CompleteLattice γ] (f : α → β) (μ : MeasureTheory.Measure α)
(g : β ≃o γ), g (essInf f μ) = essInf (fun (x : α) => g (f x)) μ
theorem
essSup_mono_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[CompleteLattice β]
{f : α → β}
(hμν : ν.AbsolutelyContinuous μ)
:
theorem
essSup_mono_measure'
{α : Type u_3}
{β : Type u_4}
:
∀ {x : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : CompleteLattice β] {f : α → β},
ν ≤ μ → essSup f ν ≤ essSup f μ
theorem
essInf_antitone_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[CompleteLattice β]
{f : α → β}
(hμν : μ.AbsolutelyContinuous ν)
:
theorem
essSup_eq_iSup
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(f : α → β)
:
theorem
essInf_eq_iInf
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(f : α → β)
:
@[simp]
theorem
essSup_count
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[CompleteLattice β]
[MeasurableSingletonClass α]
(f : α → β)
:
@[simp]
theorem
essInf_count
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[CompleteLattice β]
[MeasurableSingletonClass α]
(f : α → β)
:
theorem
essSup_comp_le_essSup_map_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{γ : Type u_3}
{mγ : MeasurableSpace γ}
{f : α → γ}
{g : γ → β}
(hf : AEMeasurable f μ)
:
essSup (g ∘ f) μ ≤ essSup g (MeasureTheory.Measure.map f μ)
theorem
MeasurableEmbedding.essSup_map_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{γ : Type u_3}
{mγ : MeasurableSpace γ}
{f : α → γ}
{g : γ → β}
(hf : MeasurableEmbedding f)
:
essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
theorem
essSup_map_measure_of_measurable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{γ : Type u_3}
{mγ : MeasurableSpace γ}
{f : α → γ}
{g : γ → β}
[MeasurableSpace β]
[TopologicalSpace β]
[SecondCountableTopology β]
[OrderClosedTopology β]
[OpensMeasurableSpace β]
(hg : Measurable g)
(hf : AEMeasurable f μ)
:
essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
theorem
essSup_map_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[CompleteLattice β]
{γ : Type u_3}
{mγ : MeasurableSpace γ}
{f : α → γ}
{g : γ → β}
[MeasurableSpace β]
[TopologicalSpace β]
[SecondCountableTopology β]
[OrderClosedTopology β]
[OpensMeasurableSpace β]
(hg : AEMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
theorem
ENNReal.essSup_piecewise
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
{s : Set α}
[DecidablePred fun (x : α) => x ∈ s]
{g : α → ENNReal}
(hs : MeasurableSet s)
:
theorem
ENNReal.essSup_indicator_eq_essSup_restrict
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → ENNReal}
(hs : MeasurableSet s)
:
theorem
ENNReal.ae_le_essSup
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : α → ENNReal)
:
@[simp]
theorem
ENNReal.essSup_eq_zero_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
:
theorem
ENNReal.essSup_const_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
{a : ENNReal}
:
theorem
ENNReal.essSup_mul_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : α → ENNReal)
(g : α → ENNReal)
:
theorem
ENNReal.essSup_add_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : α → ENNReal)
(g : α → ENNReal)
:
theorem
ENNReal.essSup_liminf_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_3}
[Countable ι]
[LinearOrder ι]
(f : ι → α → ENNReal)
:
essSup (fun (x : α) => Filter.liminf (fun (n : ι) => f n x) Filter.atTop) μ ≤ Filter.liminf (fun (n : ι) => essSup (fun (x : α) => f n x) μ) Filter.atTop
theorem
ENNReal.coe_essSup
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → NNReal}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) (MeasureTheory.ae μ) f)
:
theorem
ENNReal.essSup_restrict_eq_of_support_subset
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → ENNReal}
(hsf : Function.support f ⊆ s)
: