Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.ScalarPoissonHessianBelowTwo

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Scalar Poisson Hessian estimates below the energy exponent

The endpoint is obtained by localized duality on the odd-reflected parent cube. The small utility below is intentionally kept here: it is the exact bridge used when a compactly supported H¹₀ multiplier must be inserted into the smooth-test divergence identity.

noncomputable def HCPolySupport.CubeCalderonZygmund.sourceHessianRowRadialDatum {d : ℕ} {m : ℤ} (q : FiniteLpExponent) {u : H1Function (openCubeSet (originCube d m))} (H : HasWeakHessianOn (openCubeSet (originCube d m)) u) (i : Fin d) (n : ℕ) : CubeEuclideanL2LpField (originCube d m) q.conjugate

Package radial truncation at level n of weak Hessian row i as an L² cube datum at the conjugate of exponent q.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CubeCalderonZygmund.exists_scalarPoisson_hessianHilbertMat_normalizedCubeMeasure_le_of_lt_two (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : q.exponent.toReal < 2) : ∃ C < ⊤, ∀ (m : ℤ) (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m)) → MeasureTheory.MemLp F q.exponent (normalizedCubeMeasure (originCube d m)) → ∀ (u : H10Function (openCubeSet (originCube d m))), CubeDirichletWeakPoissonProblem (originCube d m) u F → ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function), MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure (originCube d m)) ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure (originCube d m)) ≤ C * MeasureTheory.eLpNorm F q.exponent (normalizedCubeMeasure (originCube d m))

Calderón--Zygmund Hessian estimate on centered cubes below the energy exponent. The Hessian representative is supplied by the energy estimate and its L^q bound is obtained row-by-row from the localized duality argument.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH10ScalarPoisson_hessian_cz_of_lt_two (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : q.exponent.toReal < 2) : ∃ C < ⊤, ∀ (m : ℤ) (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m)) → MeasureTheory.MemLp F q.exponent (normalizedCubeMeasure (originCube d m)) → ∀ (u : H10Function (openCubeSet (originCube d m))), CubeDirichletWeakPoissonProblem (originCube d m) u F → ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function), MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure (originCube d m)) ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure (originCube d m)) ≤ C * MeasureTheory.eLpNorm F q.exponent (normalizedCubeMeasure (originCube d m))

The centered-cube formulation of the below-two Hessian estimate.