DirichletNeumannEndpoint

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

Dirichlet and Neumann Calderón--Zygmund endpoint

This file combines the arbitrary-cube Dirichlet and mean-zero Neumann estimates under one positive real constant.

theorem HCPolySupport.CubeCalderonZygmund.exists_cubeDirichletNeumannDivergence_cz {d : ℕ} (dimension : 2 ≤ d) (p : ENNReal) (one_lt_p : 1 < p) (p_lt_top : p < ⊤) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : TriadicCube d) (f : Vec d → Vec d), MeasureTheory.MemLp f p (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 p (normalizedCubeMeasure Q) ∧ cubeLpNorm Q p u.grad ≤ C * cubeLpNorm Q p f) ∧ ∀ (u : H1MeanZeroFunction (openCubeSet Q)), (IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => 1) (openCubeSet Q) u fun (x : Vec d) => -f x) → MeasureTheory.MemLp u.toH1Function.grad p (normalizedCubeMeasure Q) ∧ cubeLpNorm Q p u.toH1Function.grad ≤ C * cubeLpNorm Q p f

The Dirichlet and mean-zero Neumann divergence-form Calderón--Zygmund estimates on arbitrary triadic cubes, with one constant depending only on the dimension and finite exponent.