Essential suprema on the support of a measure

For a nonnegative extended-valued lower semicontinuous function, its essential supremum is its pointwise supremum on the support, provided that support is conull. In particular this holds on hereditarily Lindelöf spaces, without a finiteness assumption on the measure.

This identifies essential bounds on continuous observables, such as distance from a fixed point, with geometric bounds on the support. Lower semicontinuity is important: an upward change at a single null point need not affect the essential supremum.

The file also records two facts about the essential oscillation essSup f μ - essInf f μ of a real function: a function with values in an interval of length L has essential oscillation at most L (TauCeti.essSup_sub_essInf_le), and the essential oscillation of an essentially bounded function does not increase when the measure is replaced by an absolutely continuous one, for example its restriction to a smaller set (TauCeti.essSup_sub_essInf_mono_measure). These make the essential oscillation on a ball the smallest length of an interval containing the function there, monotone in the radius, which is how oscillation decay estimates are iterated. The essential supremum of an essentially bounded real function is also the supremum of the levels that it exceeds on a set of positive measure (TauCeti.ae_le_csSup_of_bddAbove).

theorem TauCeti.essSup_eq_iSup_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} (f : X → ENNReal) (hf : LowerSemicontinuous f) (hμ : μ.support ∈ MeasureTheory.ae μ) : essSup f μ = ⨆ x ∈ μ.support, f x

The essential supremum of a lower semicontinuous nonnegative extended-valued function is its supremum on the support, whenever the support is conull.

theorem TauCeti.essSup_sub_essInf_le {α : Type u_2} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [(MeasureTheory.ae ν).NeBot] {f : α → ℝ} {m L : ℝ} (hf : ∀ᵐ (x : α) ∂ν, f x ∈ Set.Icc m (m + L)) : essSup f ν - essInf f ν ≤ L

A real function taking values almost everywhere in an interval of length L has essential oscillation at most L.

theorem TauCeti.essSup_sub_essInf_mono_measure {α : Type u_2} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [(MeasureTheory.ae ν).NeBot] {ν' : MeasureTheory.Measure α} {f : α → ℝ} (hν : ν.AbsolutelyContinuous ν') (hf₁ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (MeasureTheory.ae ν') f) (hf₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (MeasureTheory.ae ν') f) : essSup f ν - essInf f ν ≤ essSup f ν' - essInf f ν'

The essential oscillation of a real function that is essentially bounded with respect to ν' does not increase when ν' is replaced by a measure ν ≪ ν', for example by its restriction to a smaller set, provided that ν is nonzero.

theorem TauCeti.ae_le_csSup_of_bddAbove {α : Type u_2} [MeasurableSpace α] {ν : MeasureTheory.Measure α} (f : α → ℝ) {k : ℝ} (hk : ¬∀ᵐ (x : α) ∂ν, f x ≤ k) (hbdd : BddAbove {l : ℝ | k ≤ l ∧ ¬∀ᵐ (x : α) ∂ν, f x ≤ l}) : (∀ᵐ (x : α) ∂ν, f x ≤ sSup {l : ℝ | k ≤ l ∧ ¬∀ᵐ (x : α) ∂ν, f x ≤ l}) ∧ k < sSup {l : ℝ | k ≤ l ∧ ¬∀ᵐ (x : α) ∂ν, f x ≤ l}

If a real function is not almost everywhere at most k but is essentially bounded above, the levels l ≥ k that it exceeds on a set of positive measure have a supremum M; then f ≤ M almost everywhere and k < M.

theorem TauCeti.essSup_sub_essInf_nonneg_monotoneOn_ball {X : Type u_3} [PseudoMetricSpace X] [MeasurableSpace X] {mu : MeasureTheory.Measure X} [mu.IsOpenPosMeasure] (x₀ : X) {R₁ M : ℝ} {v : X → ℝ} {φ : ℝ → ℝ} (hφ : ∀ (ρ : ℝ), φ ρ = essSup v (mu.restrict (Metric.ball x₀ ρ)) - essInf v (mu.restrict (Metric.ball x₀ ρ))) (hR₁ : 0 < R₁) (hM : ∀ᵐ (x : X) ∂mu.restrict (Metric.ball x₀ R₁), |v x| ≤ M) : (∀ ρ ∈ Set.Ioc 0 R₁, 0 ≤ φ ρ) ∧ MonotoneOn φ (Set.Ioc 0 R₁) ∧ φ R₁ ≤ 2 * M

The essential oscillation φ ρ of a function v on a ball B(x₀, ρ) for an open-positive measure is nonnegative and monotone in ρ ∈ (0, R₁], and at most 2 M at R₁, if |v| ≤ M almost everywhere on B(x₀, R₁).