essSup_congr_ae
theorem essSup_congr_ae :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : ConditionallyCompleteLattice β] {f g : α → β}, μ.ae.EventuallyEq f g → essSup f μ = essSup g μ
This theorem states that for any two functions `f` and `g` from a measurable space `α` to a conditionally complete lattice `β`, and for any measure `μ` on `α`, if `f` and `g` are equal almost everywhere with respect to measure `μ`, then their essential supremum with respect to measure `μ` are also equal. Here, "almost everywhere" means that the set of points where the two functions differ has measure zero. The essential supremum of a function with respect to a measure is the smallest value `c` such that the function's value is less than or equal to `c` almost everywhere.
More concisely: If `f` and `g` are measurable functions from a measurable space `α` to a conditionally complete lattice `β`, and `μ` is a measure on `α` such that `f = g` almost everywhere with respect to `μ`, then the essential supremum of `f` and `g` with respect to `μ` are equal.
|
essSup_mono_ae
theorem essSup_mono_ae :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β]
{f g : α → β}, μ.ae.EventuallyLE f g → essSup f μ ≤ essSup g μ
The theorem `essSup_mono_ae` states that for any complete lattice `β`, measurable space `α`, measure `μ` on `α`, and two functions `f` and `g` from `α` to `β`, if `f` is less than or equal to `g` almost everywhere (with respect to the measure `μ`), then the essential supremum of `f` with respect to `μ` is less than or equal to the essential supremum of `g` with respect to `μ`.
In simpler terms, it means that if one function is generally smaller than another when you measure "most" of the places (almost everywhere), then the least upper bound or "the highest low point" (essential supremum) of the smaller function is also smaller or equal to the least upper bound of the larger function.
More concisely: If two functions from a measurable space to a complete lattice are almost everywhere ordered, then the essential supremum of the first function is less than or equal to the essential supremum of the second function.
|
essSup_eq_sInf
theorem essSup_eq_sInf :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {m : MeasurableSpace α}
(μ : MeasureTheory.Measure α) (f : α → β), essSup f μ = sInf {a | ↑↑μ {x | a < f x} = 0}
This theorem states that for any measure space `α`, and any function `f` from `α` to a conditionally complete linear order `β`, the essential supremum of `f` with respect to a measure `μ` is equal to the infimum of the set of those `a` in `β` for which the measure of the set of points `x` in `α` where `a` is less than `f(x)` is zero. Essentially, it's saying that the least upper bound of `f` almost everywhere is the greatest lower bound of the set of values that `f` exceeds almost nowhere.
More concisely: For any measure space `α`, measurable function `f` from `α` to a conditionally complete linear order `β`, and `a` in `β`, the essential supremum of `f` with respect to the measure `μ` equals `a` if and only if the measure of the set of points `x` in `α` where `f(x) < a` is zero.
|
essSup_map_measure
theorem essSup_map_measure :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β]
{γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β} [inst_1 : MeasurableSpace β]
[inst_2 : TopologicalSpace β] [inst_3 : SecondCountableTopology β] [inst_4 : OrderClosedTopology β]
[inst_5 : OpensMeasurableSpace β],
AEMeasurable g (MeasureTheory.Measure.map f μ) →
AEMeasurable f μ → essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
The theorem `essSup_map_measure` states that for any two types `α` and `β`, both equipped with a `MeasurableSpace` structure, a measure `μ` on `α`, and a `CompleteLattice` structure on `β`, and for any additional type `γ` with a `MeasurableSpace` structure, a function `f` from `α` to `γ`, and a function `g` from `γ` to `β`, where the latter also has a `TopologicalSpace` structure, a `SecondCountableTopology`, an `OrderClosedTopology`, and an `OpensMeasurableSpace` structure, if `g` is almost everywhere measurable with respect to the pushforward measure of `f` applied to `μ` and `f` is almost everywhere measurable with respect to `μ`, then the essential supremum of `g` with respect to the pushforward measure of `f` applied to `μ` is equal to the essential supremum of the composition of `g` and `f` with respect to `μ`. In other words, the essential supremum (the smallest upper bound that the function does not exceed except on a set of measure zero) is preserved under the mapping of measures.
More concisely: Given measure spaces `(α, Σα, μ)`, `(β, Σβ, μβ)`, complete lattices `(β, ≤)`, functions `f: α → γ` and `g: γ → β`, and measurable spaces `(γ, Σγ, τ)` with `μγ` being the pushforward measure of `μ` under `f`, if `g` is almost everywhere measurable with respect to `μγ` and `f` is almost everywhere measurable with respect to `μ`, then the essential supremum of `g` with respect to `μβ` equals the essential supremum of the composition `g ∘ f` with respect to `μ`.
|