CubeSchauderData

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

Cube Schauder, data layer

Nothing here is an elliptic estimate. Every declaration is a proved local helper; no source node is claimed, realized, or closed by this module.

Main results

• norm_sub_le_of_mem_openCubeSet_originCube — the sup-norm diameter of □_m is 3^m.
• holderSeminormBoundOn_lower_exponent — on a set of diameter ≤ D, a C^{0,α} bound implies a C^{0,β} bound for β ≤ α, at the constant K · D^{α-β}. This is the s ≤ 1/2 leg of the frozen gauge.
• holderSeminormBoundOn_nonneg_openCubeSet — on the open cube in dimension d ≥ 1 a Hölder bound forces its constant to be nonnegative.
• memVectorL2_of_holderSeminormBoundOn — a C^{0,α} vector field on □_m is in L²(□_m), which is what CoarseGraining's Dirichlet existence theorem consumes.

References

• ABK26, (the asserted Schauder input).
• Algsuperdiff/Frozen/External/CubeSchauder.lean (the frozen statement).

1. Sup-norm geometry of the open origin cube

theorem Algsuperdiff.Section4.Provider.Schauder.zero_mem_openCubeSet_originCube {d : ℕ} (m : ℤ) : 0 ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The origin is in every open origin cube.

theorem Algsuperdiff.Section4.Provider.Schauder.norm_sub_le_of_mem_openCubeSet_originCube {d : ℕ} {m : ℤ} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hy : y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ‖x - y‖ ≤ 3 ^ m

The sup-norm diameter of □_m is 3^m.

theorem Algsuperdiff.Section4.Provider.Schauder.quarterPoint_mem_openCubeSet_originCube {d : ℕ} (m : ℤ) : (fun (x : Fin d) => 3 ^ m / 4) ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The constant quarter point lies in □_m. Together with the origin it is the two-point witness forcing Hölder constants on the cube to be nonnegative.

2. The rpow dictionary for the triadic scale factor

theorem Algsuperdiff.Section4.Provider.Schauder.zpow_three_rpow (m : ℤ) (t : ℝ) : (3 ^ m) ^ t = Real.rpow 3 (t * ↑m)

(3^m)^t = 3^{t·m} — the passage between the integer power of the scale factor and the real power spelled in the frozen gauge.

theorem Algsuperdiff.Section4.Provider.Schauder.rpow_three_pos (t : ℝ) : 0 < Real.rpow 3 t

3. Elementary algebra of the Hölder carrier

theorem Algsuperdiff.Section4.Provider.Schauder.holderSeminormBoundOn_add {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K L : ℝ} {f g : HCPolySupport.Vec d → E} (hf : Support.HolderSeminormBoundOn U alpha K f) (hg : Support.HolderSeminormBoundOn U alpha L g) : Support.HolderSeminormBoundOn U alpha (K + L) fun (x : HCPolySupport.Vec d) => f x + g x

Hölder bounds add.

theorem Algsuperdiff.Section4.Provider.Schauder.holderSeminormBoundOn_smul_nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set (HCPolySupport.Vec d)} {alpha K c : ℝ} {f : HCPolySupport.Vec d → E} (hf : Support.HolderSeminormBoundOn U alpha K f) (hc : 0 ≤ c) : Support.HolderSeminormBoundOn U alpha (c * K) fun (x : HCPolySupport.Vec d) => c • f x

Hölder bounds scale by a nonnegative scalar.

4. Lowering the Hölder exponent on a bounded set

theorem Algsuperdiff.Section4.Provider.Schauder.holderSeminormBoundOn_lower_exponent {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha beta K D : ℝ} {f : HCPolySupport.Vec d → E} (hf : Support.HolderSeminormBoundOn U alpha K f) (hK : 0 ≤ K) (hbeta : 0 < beta) (hle : beta ≤ alpha) (hdiam : ∀ x ∈ U, ∀ y ∈ U, ‖x - y‖ ≤ D) : Support.HolderSeminormBoundOn U beta (K * D ^ (alpha - beta)) f

Exponent lowering. On a set of diameter at most D, a C^{0,α} bound with nonnegative constant K gives a C^{0,β} bound at K · D^{α-β} whenever 0 < β ≤ α. (0 < D is only used through D^{α-β} ≥ t^{α-β}.)

theorem Algsuperdiff.Section4.Provider.Schauder.holderSeminormBoundOn_lower_exponent_originCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {m : ℤ} {beta K : ℝ} {f : HCPolySupport.Vec d → E} (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) (hK : 0 ≤ K) (hbeta : 0 < beta) (hle : beta ≤ 1 / 2) : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) beta (K * Real.rpow 3 ((1 / 2 - beta) * ↑m)) f

Exponent lowering on the open origin cube, with the scale factor spelled as in the frozen gauge.

5. Continuity, boundedness and L² membership

theorem Algsuperdiff.Section4.Provider.Schauder.continuousOn_of_holderSeminormBoundOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (halpha : 0 < alpha) (hf : Support.HolderSeminormBoundOn U alpha K f) : ContinuousOn f U

A Hölder-continuous field is continuous on the domain of the bound.

theorem Algsuperdiff.Section4.Provider.Schauder.norm_le_of_holderSeminormBoundOn_originCube {d : ℕ} {m : ℤ} {alpha K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (halpha : 0 ≤ alpha) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) alpha K f) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ‖f x‖ ≤ ‖f 0‖ + K * (3 ^ m) ^ alpha

A Hölder-continuous field on □_m is bounded there by its value at the origin plus K · 3^{αm}.

theorem Algsuperdiff.Section4.Provider.Schauder.memVectorL2_of_holderSeminormBoundOn {d : ℕ} {m : ℤ} {alpha K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (halpha : 0 < alpha) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) alpha K f) : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) f

A Hölder-continuous vector field on □_m is square integrable there. This is the hypothesis CoarseGraining's Dirichlet existence theorem consumes.

6. Nonnegativity of the constants on the cube

theorem Algsuperdiff.Section4.Provider.Schauder.holderSeminormBoundOn_nonneg_openCubeSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {m : ℤ} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hd : 0 < d) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) alpha K f) : 0 ≤ K

On the open origin cube in dimension d ≥ 1, a Hölder bound forces its constant to be nonnegative: the origin and the quarter point on the first axis are two distinct points of the cube.