Representative

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

Continuous representatives on the cube y + □_n

The Section 5 error and regularity quantities measure a solution in the supremum norm and in the 1/2-Hölder seminorm, both taken pointwise on y + □_n. An H¹ witness is only determined away from a null set, so those quantities are attached not to the witness but to a continuous representative of it. This module names that datum and proves that it is unique where it is asserted.

Main definitions

• HasCubeContinuousRepresentativeAt y n u — the H¹ witness u has an everywhere-defined representative that agrees with it away from a null set and is continuous on y + □_n.

Main results

• eqOn_of_ae_eq_of_continuousOn — on an open set, two functions that agree away from a null set and are continuous there agree at every point.
• hasCubeContinuousRepresentativeAt_unique — any two representatives of the same witness agree at every point of y + □_n.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

1. Continuity pins a representative

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

On an open set, an almost-everywhere identity between two functions that are continuous there is a pointwise identity. The set where they differ is open, and a nonempty open subset of ℝ^d has positive volume.

2. The representative datum on y + □_n

def Algsuperdiff.Section5.Support.HasCubeContinuousRepresentativeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (u : HCPolySupport.H1Function (cubeSetAt y n)) : Prop

u has a representative continuous on y + □_n.

This is the datum the Section 5 regularity quantity needs in order to measure u in the 1/2-Hölder seminorm at every point of the cube, not merely away from a null set. No finiteness of that seminorm is required: where the source takes the seminorm of the continuous representative, an infinite value is a legitimate value and must be recorded as such.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Support.hasCubeContinuousRepresentativeAt_unique {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {u : HCPolySupport.H1Function (cubeSetAt y n)} {u₁ u₂ : HCPolySupport.Vec d → ℝ} (h₁ : u₁ =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] u.toFun) (hc₁ : ContinuousOn u₁ (cubeSetAt y n)) (h₂ : u₂ =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] u.toFun) (hc₂ : ContinuousOn u₂ (cubeSetAt y n)) : Set.EqOn u₁ u₂ (cubeSetAt y n)

The representative is unique on the cube. Two representatives of the same H¹ witness agree at every point of y + □_n, so every pointwise quantity built from one of them is independent of the choice.

theorem Algsuperdiff.Section5.Support.holderSeminormOn_eq_of_hasCubeContinuousRepresentativeAt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {alpha : ℝ} {u : HCPolySupport.H1Function (cubeSetAt y n)} {u₁ u₂ : HCPolySupport.Vec d → ℝ} (h₁ : u₁ =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] u.toFun) (hc₁ : ContinuousOn u₁ (cubeSetAt y n)) (h₂ : u₂ =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] u.toFun) (hc₂ : ContinuousOn u₂ (cubeSetAt y n)) : holderSeminormOn (cubeSetAt y n) alpha u₁ = holderSeminormOn (cubeSetAt y n) alpha u₂

Two representatives of the same witness have the same Hölder seminorm on the cube.