HolderCalculus

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

Calculus of the supremum norm and the Hölder seminorm

This file retains two explicit two-point estimates: interpolation of a Hölder bound between a supremum bound and a Lipschitz bound,

  [F]_{C^{0,1/2}(U)} ≤ ( 2 ‖F‖_{L^∞(U)} · L )^{1/2} ,

and the Leibniz estimate for a scalar multiple in explicit HolderSeminormBoundOn form.

References

• ABK26, the localized estimates of Section 5.1.

2. Interpolation between the supremum norm and a Lipschitz bound

theorem Algsuperdiff.Section5.Support.holderSeminormBoundOn_half_of_supNorm_of_lipschitz {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {S L : ℝ} {F : HCPolySupport.Vec d → E} (hS : ∀ x ∈ U, ‖F x‖ ≤ S) (hL : Section4.Support.HolderSeminormBoundOn U 1 L F) : Section4.Support.HolderSeminormBoundOn U (1 / 2) (√(2 * S * L)) F

Interpolation of the 1/2-Hölder seminorm. A field bounded by S on U and Lipschitz there with constant L has 1/2-Hölder seminorm at most (2 S L)^{1/2}: the two bounds ‖F x - F z‖ ≤ 2S and ‖F x - F z‖ ≤ L‖x - z‖ multiply, and the square root of their product is the stated bound.

No sign hypothesis is needed: at two distinct points of U the two hypotheses force 0 ≤ S and 0 ≤ L, and at a single point both sides vanish.

3. The Leibniz rule

theorem Algsuperdiff.Section5.Support.holderSeminormBoundOn_smul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set (HCPolySupport.Vec d)} {alpha Kf Sf KG SG : ℝ} {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → E} (hKf0 : 0 ≤ Kf) (hSf0 : 0 ≤ Sf) (hKf : Section4.Support.HolderSeminormBoundOn U alpha Kf f) (hSf : ∀ x ∈ U, ‖f x‖ ≤ Sf) (hKG : Section4.Support.HolderSeminormBoundOn U alpha KG G) (hSG : ∀ x ∈ U, ‖G x‖ ≤ SG) : Section4.Support.HolderSeminormBoundOn U alpha (Kf * SG + Sf * KG) fun (x : HCPolySupport.Vec d) => f x • G x

The Leibniz rule in explicit two-point form. With a Hölder constant and a supremum bound for each factor, the product obeys the Hölder bound with constant Kf · SG + Sf · KG.