HolderGauge

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

The Hölder seminorm and supremum norm

Section 5 measures its forcing fields and its solutions in two gauges: the supremum norm ‖·‖_{L^∞(y+□_n)} and the 1/2-Hölder seminorm [·]_{C^{0,1/2}(y+□_n)}. Both are stated here as ℝ≥0∞-valued quantities, so that an unbounded family has the value ⊤ rather than silently collapsing, and both are stated for maps into an arbitrary normed group E, so that the scalar case (a solution u) and the vector case (a forcing field g : Vec d → Vec d) are one declaration. The basic lemmas below identify bounds on these extended-real suprema with pointwise real inequalities.

References

• ABK26, the function-space conventions and the localized estimates of Section 5.1.

1. The two gauges

noncomputable def Algsuperdiff.Section5.Support.holderSeminormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (U : Set (HCPolySupport.Vec d)) (alpha : ℝ) (f : HCPolySupport.Vec d → E) : ENNReal

[f]_{C^{0,α}(U)}, the α-Hölder seminorm of f on U, as an element of ℝ≥0∞: the supremum of the difference quotients ‖f x - f z‖ / ‖x - z‖^α over distinct pairs of points of U. The value is ⊤ exactly when the family of quotients is unbounded.

Equations

• Algsuperdiff.Section5.Support.holderSeminormOn U alpha f = ⨆ x ∈ U, ⨆ z ∈ U, ⨆ (_ : x ≠ z), ENNReal.ofReal (‖f x - f z‖ / ‖x - z‖ ^ alpha)

noncomputable def Algsuperdiff.Section5.Support.supNormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (U : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → E) : ENNReal

‖f‖_{L^∞(U)} read pointwise: the supremum of ‖f x‖ over x ∈ U, as an element of ℝ≥0∞. This is the pointwise supremum, not the essential supremum; Section 5 applies it to a continuous representative, for which the two agree on an open set.

Equations

• Algsuperdiff.Section5.Support.supNormOn U f = ⨆ x ∈ U, ENNReal.ofReal ‖f x‖

theorem Algsuperdiff.Section5.Support.supNormOn_le_iff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → E} {c : ENNReal} : supNormOn U f ≤ c ↔ ∀ x ∈ U, ENNReal.ofReal ‖f x‖ ≤ c

theorem Algsuperdiff.Section5.Support.le_supNormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → E} {x : HCPolySupport.Vec d} (hx : x ∈ U) : ENNReal.ofReal ‖f x‖ ≤ supNormOn U f

theorem Algsuperdiff.Section5.Support.supNormOn_le_ofReal_iff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {K : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) : supNormOn U f ≤ ENNReal.ofReal K ↔ ∀ x ∈ U, ‖f x‖ ≤ K

The supremum norm is bounded by an explicit constant exactly when the pointwise bound holds.

theorem Algsuperdiff.Section5.Support.le_holderSeminormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha : ℝ} {f : HCPolySupport.Vec d → E} {x z : HCPolySupport.Vec d} (hx : x ∈ U) (hz : z ∈ U) (hne : x ≠ z) : ENNReal.ofReal (‖f x - f z‖ / ‖x - z‖ ^ alpha) ≤ holderSeminormOn U alpha f

2. The seminorm bound is the two-point bound

theorem Algsuperdiff.Section5.Support.holderSeminormOn_le_ofReal_iff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hK : 0 ≤ K) : holderSeminormOn U alpha f ≤ ENNReal.ofReal K ↔ Section4.Support.HolderSeminormBoundOn U alpha K f

The bridge between the ℝ≥0∞ seminorm and the explicit two-point bound. No hypothesis on the exponent alpha is needed: the diagonal pair contributes nothing to the supremum, and on the diagonal the two-point bound is automatic from 0 ≤ K.