CubeSchauderCore

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

Cube Schauder: the zero-datum core and the assembly at the frozen brackets

ZeroDatumCubeSchauder d C0 is the zero-datum, unit-diffusivity interior + boundary C^{1,1/2} statement on the origin cubes: for a C^{0,1/2} forcing G there is an H¹₀(□_m) solution of -Δw = ∇·G whose own gradient representative satisfies

  ‖∇w‖_{L^∞(□_m)} ≤ C0 · 3^{m/2} · [G]_{C^{0,1/2}(□_m)} ,
  [∇w]_{C^{0,1/2}(□_m)} ≤ C0 · [G]_{C^{0,1/2}(□_m)} .

cube_schauder_of_zeroDatumCubeSchauder derives from it the byte-exact body of the frozen external Algsuperdiff.Frozen.External.cube_schauder, with C(d,s) = 2· + 1 produced before the scale, the diffusivity and the data. The three reductions performed here are the route's steps (b), (e) and the s ≤ 1/2 interpolation:

• diffusivity (linearity): -sigma Δ v = ∇·g is -Δ v = ∇·(sigma⁻¹ g);
• datum (affine shift): w := v - h solves the zero-datum problem at the forcing G := sigma⁻¹ g + ∇h, whose C^{0,1/2} seminorm is at most sigma⁻¹ Kg + Kh;
• exponent: on a set of diameter 3^m, [·]_{C^{0,s}} ≤ 3^{(1/2-s)m} [·]_{C^{0,1/2}}, which is exactly the weight the frozen gauge carries.

The scale uniformity is not reduced away: ZeroDatumCubeSchauder quantifies over all m : ℤ with one constant, because the interior/boundary proof is naturally scale-aware on the triadic carriers.

References

• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.
• Armstrong--Kuusi, Elliptic Regularity (ellipticregularity.tex), Proposition p.Schauder.C1alpha — the interior route the residual core follows.

1. The residual core

def Algsuperdiff.Section4.Provider.Schauder.ZeroDatumCubeSchauder (d : ℕ) (C0 : ℝ) : Prop

The zero-datum, unit-diffusivity cube Schauder core.

For every scale m and every C^{0,1/2} forcing G on □_m there is an H¹₀(□_m) weak solution of -Δ w = ∇·G whose own gradient representative is bounded · 3^{m/2} · KGandC^{0,1/2} with constant · KG.

This is the interior + boundary estimate of the author's route (steps (c), (d)): interior C^{1,α} off the pointwise C^{1,1} estimates for harmonic functions, boundary by odd reflection across the met faces, corners by iterated partial reflections. It is stated for all m with one constant, so scale uniformity is part of the core rather than a separate reduction.

Equations

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

2. The rpow identities of the gauge

theorem Algsuperdiff.Section4.Provider.Schauder.rpow_three_neg (t : ℝ) : Real.rpow 3 (-t) = (Real.rpow 3 t)⁻¹

theorem Algsuperdiff.Section4.Provider.Schauder.rpow_three_half_sub (s : ℝ) (m : ℤ) : Real.rpow 3 ((1 / 2 - s) * ↑m) = Real.rpow 3 (↑m / 2) * (Real.rpow 3 (s * ↑m))⁻¹

The gauge weight factorizes: 3^{(1/2-s)m} = 3^{m/2} · (3^{sm})⁻¹.

3. The assembly

theorem Algsuperdiff.Section4.Provider.Schauder.cube_schauder_of_zeroDatumCubeSchauder {d : ℕ} {C0 : ℝ} (hC0 : 0 ≤ C0) (hcore : ZeroDatumCubeSchauder d C0) (dimension : 2 ≤ d) (s : ℝ) (s_pos : 0 < s) (s_le : s ≤ 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ℤ) (sigma : ℝ), 0 < sigma → ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (Kg KhInf Kh : ℝ), Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → ∃ (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v h g ∧ ∃ (Ksup : ℝ) (KHol : ℝ), 0 ≤ Ksup ∧ 0 ≤ KHol ∧ (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖v.grad x‖ ≤ Ksup) ∧ Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s KHol v.grad ∧ Real.rpow 3 (-(s * ↑m)) * Ksup + KHol ≤ C * (Real.rpow 3 (s * ↑m))⁻¹ * (sigma⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))

The frozen cube Schauder conclusion, off the zero-datum core.

The constant C(d,s) = 2· + 1 is produced before the scale m, the diffusivity sigma and the data, so the consumer's constant scope is the frozen statement's own. Nothing but ZeroDatumCubeSchauder d and 0 ≤ is assumed.