FiniteLpLpData

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

Supplied-solution cube Calderón--Zygmund estimates for L^p data

This file removes the auxiliary L² assumption on the datum in the centered-cube finite-exponent Calderón--Zygmund estimate. Below exponent two the proof uses the existing adjoint-duality argument directly. At and above exponent two, finite normalized cube volume supplies the required L² membership internally.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH10ScalarDivergence_cz_lpData (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanLpField (originCube d m) q) (u : H10Function (openCubeSet (originCube d m))), 0 < sigma0 → (∀ (psi : H10Function (openCubeSet (originCube d m))), sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (u.grad x) (psi.grad x) = -∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (h.toField x) (psi.grad x)) → (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent u.grad ≤ C * (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent h.toField

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