EssentialSupremum

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

On an open set the essential supremum of a continuous function is its supremum

The L^∞ norm of a Sobolev function on an open set is an essential supremum: it does not see a null set, so it is attached to the almost-everywhere class and not to any pointwise choice. When the class has a representative continuous on the open set, the essential supremum is the pointwise supremum of that representative: the two inequalities are the almost-everywhere bound in one direction and, in the other, the fact that a nonempty open subset of ℝ^d has positive volume, so no continuous function can exceed its essential supremum on a null set only.

This is what lets the localized error of Section 5.1 be stated as the honest essential supremum of the Sobolev functions while still being computed, where a continuous representative exists, from pointwise values.

Main results

• eLpNorm_top_restrict_le_supNormOn — the elementary direction.
• supNormOn_le_eLpNorm_top_restrict — the direction that uses continuity.
• eLpNorm_top_restrict_eq_supNormOn, eLpNorm_top_restrict_eq_supNormOn_of_ae.

References

• ABK26, the localized error of Section 5.1.

theorem Algsuperdiff.Section5.Support.eLpNorm_top_restrict_le_supNormOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (f : HCPolySupport.Vec d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict U)) : MeasureTheory.eLpNorm f ⊤ (MeasureTheory.volume.restrict U) ≤ supNormOn U f

The essential supremum never exceeds the pointwise supremum.

theorem Algsuperdiff.Section5.Support.supNormOn_le_eLpNorm_top_restrict {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {f : HCPolySupport.Vec d → ℝ} (hf : ContinuousOn f U) : supNormOn U f ≤ MeasureTheory.eLpNorm f ⊤ (MeasureTheory.volume.restrict U)

On an open set a continuous function does not exceed its essential supremum. Otherwise it would exceed it on a nonempty open set, which has positive volume.

theorem Algsuperdiff.Section5.Support.eLpNorm_top_restrict_eq_supNormOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {f : HCPolySupport.Vec d → ℝ} (hf : ContinuousOn f U) : MeasureTheory.eLpNorm f ⊤ (MeasureTheory.volume.restrict U) = supNormOn U f

The L^∞ norm on an open set is the supremum of a continuous representative.

theorem Algsuperdiff.Section5.Support.eLpNorm_top_restrict_eq_supNormOn_of_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {f g : HCPolySupport.Vec d → ℝ} (hae : g =ᵐ[MeasureTheory.volume.restrict U] f) (hg : ContinuousOn g U) : MeasureTheory.eLpNorm f ⊤ (MeasureTheory.volume.restrict U) = supNormOn U g

The same, reading the L^∞ norm of a function through a continuous function equal to it away from a null set.