NeumannEndpoint

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Arbitrary-cube Neumann Calderón--Zygmund endpoint

This file translates the centered finite-exponent Neumann estimate to an arbitrary triadic cube and exposes it on the project's raw Vec norm. The datum needs only the stated finite-Lᵖ membership.

theorem HCPolySupport.CubeCalderonZygmund.exists_cubeH1MeanZeroNeumannDivergence_cz (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : TriadicCube d) (f : Vec d → Vec d), MeasureTheory.MemLp f q.exponent (normalizedCubeMeasure Q) → ∀ (u : H1MeanZeroFunction (openCubeSet Q)), (IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => 1) (openCubeSet Q) u fun (x : Vec d) => -f x) → MeasureTheory.MemLp u.toH1Function.grad q.exponent (normalizedCubeMeasure Q) ∧ cubeLpNorm Q q.exponent u.toH1Function.grad ≤ C * cubeLpNorm Q q.exponent f

The raw-vector mean-zero Neumann Calderón--Zygmund estimate on arbitrary triadic cubes. The real constant depends only on dimension and exponent.