FiniteLpBelowTwo

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

Below-two Neumann cube Calderón--Zygmund estimate

This file proves the adjoint-duality branch for a supplied mean-zero Neumann solution with only L^p datum, then combines it with the energy and good-λ branches to cover every finite exponent.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH1MeanZeroNeumannDivergence_cz_lpData_of_lt_two (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : q.exponent.toReal < 2) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanLpField (originCube d m) q) (u : H1MeanZeroFunction (openCubeSet (originCube d m))), 0 < sigma0 → (IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h.toField x) → (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent u.toH1Function.grad ≤ C * (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent h.toField

The below-two supplied-solution Neumann CZ estimate with L^p-only datum.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH1MeanZeroNeumannDivergence_cz_lpData (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanLpField (originCube d m) q) (u : H1MeanZeroFunction (openCubeSet (originCube d m))), 0 < sigma0 → (IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h.toField x) → (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent u.toH1Function.grad ≤ C * (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent h.toField

The supplied-solution centered-cube Neumann Calderón--Zygmund estimate for every finite exponent and an L^p datum. No auxiliary L² hypothesis is exposed.