HomCGFinalExtend

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

The McShane extension of a Hölder field, with the sup bound preserved

What this file supplies

The measurement named a second "absent analytic input": a smooth-test approximation of a merely Hölder field on □_m, preserving both the sup bound and the Hölder bound. This file is its first half: the extension of a C^{0,α} field from an arbitrary nonempty set A to all of Vec d, at the SAME two constants.

The construction is McShane's, applied coordinatewise and then clamped:

  φ(x)_i  =  clamp_{K_sup} ( inf_{y ∈ A} ( φ(y)_i + K_Höl ‖x - y‖^α ) ).

Three facts, in the ambient supremum metric of Vec d:

• holderExtend_eq_of_mem — φ = φ on A (the clamp is inert there because |φ(x)_i| ≤ ‖φ(x)‖ ≤ K_sup, and the infimum is attained at y = x);
• norm_holderExtend_le — ‖φ(x)‖ ≤ K_sup everywhere, by construction;
• holderSeminormBoundOn_univ_holderExtend — φ is α-Hölder on all of Vec d at the same constant K_Höl.

The Hölder half needs α ≤ 1 exactly once, for the subadditivity (a+b)^α ≤ a^α + b^α (Real.rpow_add_le_add_rpow); the sup half needs nothing beyond 0 ≤ K_sup, because clamping is a 1-Lipschitz retraction of ℝ onto [-K_sup, K_sup].

Nothing here is specific to a cube, to a fractional Sobolev carrier, or to the homogenization lane: it is the pure extension statement.

1. Clamping to a symmetric interval

def Algsuperdiff.Section4.Provider.Homogenization.clampAbs (B t : ℝ) : ℝ

The 1-Lipschitz retraction of ℝ onto [-B, B].

Equations

• Algsuperdiff.Section4.Provider.Homogenization.clampAbs B t = max (-B) (min B t)

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_clampAbs_le {B : ℝ} (hB : 0 ≤ B) (t : ℝ) : |clampAbs B t| ≤ B

The clamp lands in [-B, B].

theorem Algsuperdiff.Section4.Provider.Homogenization.clampAbs_eq_self {B t : ℝ} (h : |t| ≤ B) : clampAbs B t = t

The clamp is inert on [-B, B].

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_clampAbs_sub_clampAbs_le (B t u : ℝ) : |clampAbs B t - clampAbs B u| ≤ |t - u|

The clamp is 1-Lipschitz.

2. The McShane infimum of a scalar Hölder datum

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.mcShaneInf {d : ℕ} (A : Set (HCPolySupport.Vec d)) (K alpha : ℝ) (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : ℝ

McShane's infimum, in the ambient supremum metric: m(x) = inf_{y ∈ A} (f(y) + K‖x - y‖^α).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.mcShaneInf A K alpha f x = ⨅ (y : ↑A), f ↑y + K * ‖x - ↑y‖ ^ alpha

theorem Algsuperdiff.Section4.Provider.Homogenization.mcShaneInf_le {d : ℕ} {A : Set (HCPolySupport.Vec d)} {K alpha B : ℝ} {f : HCPolySupport.Vec d → ℝ} (hK : 0 ≤ K) (hf : ∀ y ∈ A, |f y| ≤ B) (x : HCPolySupport.Vec d) {y : HCPolySupport.Vec d} (hy : y ∈ A) : mcShaneInf A K alpha f x ≤ f y + K * ‖x - y‖ ^ alpha

The infimum is below every member of the family.

theorem Algsuperdiff.Section4.Provider.Homogenization.le_mcShaneInf {d : ℕ} {A : Set (HCPolySupport.Vec d)} {K alpha c : ℝ} {f : HCPolySupport.Vec d → ℝ} (hA : A.Nonempty) (x : HCPolySupport.Vec d) (h : ∀ y ∈ A, c ≤ f y + K * ‖x - y‖ ^ alpha) : c ≤ mcShaneInf A K alpha f x

A uniform lower bound on the family bounds the infimum.

theorem Algsuperdiff.Section4.Provider.Homogenization.mcShaneInf_eq_of_mem {d : ℕ} {A : Set (HCPolySupport.Vec d)} {K alpha B : ℝ} {f : HCPolySupport.Vec d → ℝ} (hK : 0 ≤ K) (halpha : alpha ≠ 0) (hf : ∀ y ∈ A, |f y| ≤ B) (hhol : ∀ y ∈ A, ∀ z ∈ A, |f y - f z| ≤ K * ‖y - z‖ ^ alpha) {x : HCPolySupport.Vec d} (hx : x ∈ A) : mcShaneInf A K alpha f x = f x

The extension is an extension: on A the McShane infimum returns f.

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_mcShaneInf_sub_le {d : ℕ} {A : Set (HCPolySupport.Vec d)} {K alpha B : ℝ} {f : HCPolySupport.Vec d → ℝ} (hK : 0 ≤ K) (ha0 : 0 ≤ alpha) (ha1 : alpha ≤ 1) (hA : A.Nonempty) (hf : ∀ y ∈ A, |f y| ≤ B) (x x' : HCPolySupport.Vec d) : |mcShaneInf A K alpha f x - mcShaneInf A K alpha f x'| ≤ K * ‖x - x'‖ ^ alpha

The McShane infimum is α-Hölder at the same constant, on all of Vec d.

3. The coordinatewise extension of a vector field

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.holderExtend {d : ℕ} (A : Set (HCPolySupport.Vec d)) (Ksup KHol alpha : ℝ) (phi : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The McShane extension of a Hölder vector field, coordinatewise, clamped to the sup bound.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.holderExtend_apply {d : ℕ} (A : Set (HCPolySupport.Vec d)) (Ksup KHol alpha : ℝ) (phi : HCPolySupport.Vec d → HCPolySupport.Vec d) (x : HCPolySupport.Vec d) (i : Fin d) : holderExtend A Ksup KHol alpha phi x i = clampAbs Ksup (mcShaneInf A KHol alpha (fun (y : HCPolySupport.Vec d) => phi y i) x)

theorem Algsuperdiff.Section4.Provider.Homogenization.holderExtend_eq_of_mem {d : ℕ} {A : Set (HCPolySupport.Vec d)} {Ksup KHol alpha : ℝ} {phi : HCPolySupport.Vec d → HCPolySupport.Vec d} (hKHol : 0 ≤ KHol) (halpha : alpha ≠ 0) (hsup : ∀ x ∈ A, ‖phi x‖ ≤ Ksup) (hhol : Support.HolderSeminormBoundOn A alpha KHol phi) {x : HCPolySupport.Vec d} (hx : x ∈ A) : holderExtend A Ksup KHol alpha phi x = phi x

φ = φ on A.

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_holderExtend_le {d : ℕ} {A : Set (HCPolySupport.Vec d)} {Ksup KHol alpha : ℝ} {phi : HCPolySupport.Vec d → HCPolySupport.Vec d} (hKsup : 0 ≤ Ksup) (x : HCPolySupport.Vec d) : ‖holderExtend A Ksup KHol alpha phi x‖ ≤ Ksup

‖φ‖ ≤ K_sup everywhere.

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_univ_holderExtend {d : ℕ} {A : Set (HCPolySupport.Vec d)} {Ksup KHol alpha : ℝ} {phi : HCPolySupport.Vec d → HCPolySupport.Vec d} (hKHol : 0 ≤ KHol) (ha0 : 0 ≤ alpha) (ha1 : alpha ≤ 1) (hA : A.Nonempty) (hsup : ∀ x ∈ A, ‖phi x‖ ≤ Ksup) : Support.HolderSeminormBoundOn Set.univ alpha KHol (holderExtend A Ksup KHol alpha phi)

φ is α-Hölder on all of Vec d at the constant K_Höl.