Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.ScalarPoissonHessianTwo

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

Scalar Poisson Hessian estimate at the energy exponent

The centered-cube Dirichlet H² endpoint supplies a weak Hessian with a dimension-only normalized Frobenius estimate. This file restates that endpoint for the project's Hilbert matrix realization.

theorem HCPolySupport.CubeCalderonZygmund.exists_scalarPoisson_hessianHilbertMat_normalizedCubeMeasure_le_two (d : ℕ) [NeZero d] : ∃ C < ⊤, ∀ (m : ℤ) (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (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) 2 (normalizedCubeMeasure (originCube d m)) ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) 2 (normalizedCubeMeasure (originCube d m)) ≤ C * MeasureTheory.eLpNorm F 2 (normalizedCubeMeasure (originCube d m))

The normalized L² Hessian estimate for zero-trace scalar Poisson solutions on centered triadic cubes, expressed in the Hilbert matrix carrier.