Documentation

Mathlib.MeasureTheory.Function.EssSup

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
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
    Instances For
      theorem essSup_congr_ae {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] {f : αβ} {g : αβ} (hfg : f =ᵐ[μ] g) :
      essSup f μ = essSup g μ
      theorem essInf_congr_ae {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] {f : αβ} {g : αβ} (hfg : f =ᵐ[μ] g) :
      essInf f μ = essInf g μ
      @[simp]
      theorem essSup_const' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] [NeZero μ] (c : β) :
      essSup (fun (x : α) => c) μ = c
      @[simp]
      theorem essInf_const' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] [NeZero μ] (c : β) :
      essInf (fun (x : α) => c) μ = c
      theorem essSup_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] (c : β) (hμ : μ 0) :
      essSup (fun (x : α) => c) μ = c
      theorem essInf_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] (c : β) (hμ : μ 0) :
      essInf (fun (x : α) => c) μ = c
      @[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 : αβ) :
      essSup f (c μ) = essSup 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)) :
      essSup f μ = ⨆ (a : α), f a
      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)) :
      essInf f μ = ⨅ (a : α), f a
      @[simp]
      theorem essSup_count_eq_ciSup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [ConditionallyCompleteLattice β] {f : αβ} [Nonempty α] [MeasurableSingletonClass α] (hf : BddAbove (Set.range f)) :
      essSup f MeasureTheory.Measure.count = ⨆ (a : α), f a
      @[simp]
      theorem essInf_count_eq_ciInf {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [ConditionallyCompleteLattice β] {f : αβ} [Nonempty α] [MeasurableSingletonClass α] (hf : BddBelow (Set.range f)) :
      essInf f MeasureTheory.Measure.count = ⨅ (a : α), f a
      @[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 : αβ) :
      essSup f μ = sInf {a : β | μ {x : α | a < f x} = 0}
      theorem essInf_eq_sSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αβ) :
      essInf f μ = sSup {a : β | μ {x : α | f x < a} = 0}
      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✝) :
      ∀ᵐ (y : α) ∂μ, f y essSup f μ
      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✝) :
      ∀ᵐ (y : α) ∂μ, essInf f μ f y
      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✝) :
      μ {y : α | essSup f μ < f y} = 0
      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✝) :
      μ {y : α | f y < essInf f μ} = 0
      @[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) :
      essSup f μ essSup g μ
      theorem essInf_mono_ae {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] {f : αβ} {g : αβ} (hfg : f ≤ᵐ[μ] g) :
      essInf f μ essInf 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) :
      essSup f μ 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) :
      c essInf f μ
      theorem essSup_const_bot {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] :
      essSup (fun (x : α) => ) μ =
      theorem essInf_const_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] :
      essInf (fun (x : α) => ) μ =
      theorem OrderIso.essSup_apply {α : Type u_1} {β : Type u_2} [CompleteLattice β] {m : MeasurableSpace α} {γ : Type u_3} [CompleteLattice γ] (f : αβ) (μ : MeasureTheory.Measure α) (g : β ≃o γ) :
      g (essSup f μ) = essSup (fun (x : α) => g (f x)) μ
      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 μ) :
      essSup f ν essSup f μ
      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 ν) :
      essInf f ν essInf f μ
      theorem essSup_eq_iSup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] (hμ : ∀ (a : α), μ {a} 0) (f : αβ) :
      essSup f μ = ⨆ (i : α), f i
      theorem essInf_eq_iInf {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] (hμ : ∀ (a : α), μ {a} 0) (f : αβ) :
      essInf f μ = ⨅ (i : α), f i
      @[simp]
      theorem essSup_count {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [CompleteLattice β] [MeasurableSingletonClass α] (f : αβ) :
      essSup f MeasureTheory.Measure.count = ⨆ (i : α), f i
      @[simp]
      theorem essInf_count {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [CompleteLattice β] [MeasurableSingletonClass α] (f : αβ) :
      essInf f MeasureTheory.Measure.count = ⨅ (i : α), f i
      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 μ) :
      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) :
      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 μ) :
      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 μ) :
      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) :
      essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict s))
      theorem ENNReal.essSup_indicator_eq_essSup_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hs : MeasurableSet s) :
      essSup (s.indicator f) μ = essSup f (μ.restrict s)
      theorem ENNReal.ae_le_essSup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αENNReal) :
      ∀ᵐ (y : α) ∂μ, f y essSup f μ
      @[simp]
      theorem ENNReal.essSup_eq_zero_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} :
      essSup f μ = 0 f =ᵐ[μ] 0
      theorem ENNReal.essSup_const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {a : ENNReal} :
      essSup (fun (x : α) => a * f x) μ = a * essSup f μ
      theorem ENNReal.essSup_mul_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αENNReal) (g : αENNReal) :
      essSup (f * g) μ essSup f μ * essSup g μ
      theorem ENNReal.essSup_add_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : αENNReal) (g : αENNReal) :
      essSup (f + g) μ essSup f μ + essSup g μ
      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) :
      (essSup f μ) = essSup (fun (x : α) => (f x)) μ
      theorem ENNReal.essSup_restrict_eq_of_support_subset {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αENNReal} (hsf : Function.support f s) :
      essSup f (μ.restrict s) = essSup f μ