FiniteLpAboveTwo

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

Centered-cube Neumann Calderón--Zygmund estimates above two

This file closes the reflected Neumann good-lambda estimate by layer-cake integration. Its public endpoint exposes only the supplied mean-zero weak solution and the normalized finite-exponent datum.

noncomputable def HCPolySupport.CubeCalderonZygmund.finiteLpExponentSuccNeumann (p : FiniteLpExponent) : FiniteLpExponent

The finite exponent one larger than the supplied finite exponent.

Equations

• HCPolySupport.CubeCalderonZygmund.finiteLpExponentSuccNeumann p = { exponent := p.exponent + 1, one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH1MeanZeroNeumannDivergence_cz_of_two_lt (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanL2LpField (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

Centered-cube Neumann Calderón--Zygmund estimate above the energy exponent.