Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.ScalarPoissonHessianAboveTwo

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

Scalar Poisson Hessian estimates above the energy exponent

This file integrates the source-facing one-level Hessian-row estimate. The good-lambda parameters, weak Hessian, reflected problem, cutoff, and low-level estimate are all chosen internally.

noncomputable def HCPolySupport.CubeCalderonZygmund.exponentSucc (q : FiniteLpExponent) : FiniteLpExponent

Increase the Hessian estimate exponent by one, preserving finiteness and the lower bound one.

Equations

• HCPolySupport.CubeCalderonZygmund.exponentSucc q = { exponent := q.exponent + 1, one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.exists_scalarPoisson_hessianHilbertMat_normalizedCubeMeasure_le_of_two_lt (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : ∃ 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))

Above the energy exponent, scalar Dirichlet Poisson data have a weak Hessian whose full Hilbert-matrix normalized L^q norm is controlled by the normalized scalar datum norm, uniformly over the centered-cube scale.