DirichletEndpoint

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

Arbitrary-cube Dirichlet Calderón--Zygmund endpoint

This file translates the centered finite-exponent 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; no auxiliary L² premise is exported.

theorem HCPolySupport.CubeCalderonZygmund.exists_cubeDirichletDivergence_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 : H10Function (openCubeSet Q)), (IsZeroTraceDirichletRhsWeakSolution (fun (x : Vec d) => 1) (openCubeSet Q) u fun (x : Vec d) => -f x) → MeasureTheory.MemLp u.grad q.exponent (normalizedCubeMeasure Q) ∧ cubeLpNorm Q q.exponent u.grad ≤ C * cubeLpNorm Q q.exponent f

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