FreshShellCZ

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

Step (i) of e.nablaw.in.L.eight: the Calderon-Zygmund line

The first inequality of ABK26's display e.nablaw.in.L.eight is

  ‖∇w_D‖²_{L^8(cu_K)} + ‖∇w_N‖²_{L^8(cu_K)}
      <=  C ‖forcing‖²_{L^8(cu_K)} ,

for the Dirichlet and Neumann problems e.def.w with constant-coefficient Laplacian. The manuscript's only justification is "By Calder'on-Zygmund estimates"; in this repository that is the author-designated external input

Everything in this module therefore reaches that one anchor and no other, and carries the standard three axioms [propext, Classical.choice, Quot.sound].

What this module adds over the frozen theorem

1. The frozen theorem is stated in the ambient sup gauge of Vec d = Fin d -> ℝ. The manuscript's L^8 norm of a gradient is the Euclidean one. This module carries the conversion explicitly, through CubeEuclideanL8, at the cost of one factor sqrt d on each side, which the dimension-only constant absorbs.
2. The frozen theorem bounds one solution at a time. ABK26 needs the sum of a Dirichlet and a Neumann square, and its two lanes may carry different forcings (directions e and e'). The theorem below is therefore stated with two independent forcings.
3. The frozen theorem demands MemLp of the forcing. Here it is discharged from continuity, which is what the actual fresh-shell forcing supplies.

References

• ABK26, e.nablaw.in.L.eight (first inequality).
• ABK26, e.def.w (the two corrector problems).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le {d : ℕ} (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : HCPolySupport.TriadicCube d) (fD fN : HCPolySupport.Vec d → HCPolySupport.Vec d), Continuous fD → Continuous fN → ∀ (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)), (HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) wD fun (x : HCPolySupport.Vec d) => -fD x) → ∀ (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)), (HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) wN fun (x : HCPolySupport.Vec d) => -fN x) → cubeEuclideanLpNorm Q 8 wD.grad ^ 2 + cubeEuclideanLpNorm Q 8 wN.toH1Function.grad ^ 2 ≤ C * (cubeEuclideanLpNorm Q 8 fD ^ 2 + cubeEuclideanLpNorm Q 8 fN ^ 2)

Step (i) of e.nablaw.in.L.eight.

There is one dimension-only constant such that, on every triadic cube, the zero-trace Dirichlet and mean-zero Neumann weak solutions of -Delta w = div f with continuous forcings satisfy

  ‖∇w_D‖²_{L^8} + ‖∇w_N‖²_{L^8}  <=  C ( ‖f_D‖²_{L^8} + ‖f_N‖²_{L^8} ) ,

all four norms being the manuscript's volume-normalized Euclidean L^8 norms. The constant is produced once, before the cube, the forcings and the solutions, so its dimension-only scope is part of the statement.