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

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

Finite-exponent scalar Poisson Hessian estimates

This module provides the common centered-cube scalar Poisson Hessian Calderón--Zygmund estimate for every finite exponent.

Main results

• exists_scalarPoisson_hessianHilbertMat_normalizedCubeMeasure_le: the normalized Hilbert-matrix Hessian estimate for scalar Dirichlet Poisson solutions with data in L² ∩ L^q.

Implementation notes

The proof selects the below-energy duality theorem, the energy theorem, or the above-energy good-λ theorem according to the exponent.

theorem HCPolySupport.CubeCalderonZygmund.exists_scalarPoisson_hessianHilbertMat_normalizedCubeMeasure_le (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ 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 normalized finite-exponent Calderón--Zygmund Hessian estimate for zero-trace scalar Poisson solutions on centered triadic cubes.