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

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

Fixed-radius interior weak Hessians for harmonic functions

This is an internal regularity-engine wrapper around the existing difference-quotient construction. It fixes all geometric radii, so callers of the harmonic regularity chain need provide neither cutoffs nor forcing integrability nor a Hessian witness.

noncomputable def HCPolySupport.CubeCalderonZygmund.innerHalfSevenTwelfthCutoff {d : ℕ} (Q : TriadicCube d) : QuantitativeCubeCutoff Q (1 / 2) (7 / 12)

Internal cutoff from the half cube to the seven-twelfths cube, leaving a strict margin inside the two-thirds ambient region.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.outerThreeQuarterSevenEighthCutoff {d : ℕ} (Q : TriadicCube d) : QuantitativeCubeCutoff Q (3 / 4) (7 / 8)

Internal outer cutoff used by the fixed-radius interior construction.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.exists_innerHalf_hasWeakHessianOn_harmonic {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (h : WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) : ∃ (uS : H1Function (scaledOpenCubeSet Q (1 / 2))), uS.toFun = u.toFun ∧ uS.grad = u.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q (1 / 2)) uS), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound u (fun (x : Vec d) => 0) i (outerThreeQuarterSevenEighthCutoff Q)

A weakly harmonic H¹ function on a triadic cube has the canonical strict-interior weak Hessian supplied by the existing difference-quotient theorem.

noncomputable def HCPolySupport.CubeCalderonZygmund.HasWeakHessianOn.addConst {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1Function U} (H : HasWeakHessianOn U u) (c : ℝ) : HasWeakHessianOn U (u.addConst c)

A constant shift of the value representative keeps a weak Hessian with the same coordinate fields.

Equations

• HCPolySupport.CubeCalderonZygmund.HasWeakHessianOn.addConst H c = { hess := H.hess, hess_memL2 := ⋯, weak_second := ⋯ }

noncomputable def HCPolySupport.CubeCalderonZygmund.harmonicInteriorHessianEnergyCoreConstant (d : ℕ) : ℝ

The dimension-dependent square-root constant combining cutoff gradient and mean-zero coercivity bounds in the harmonic interior Hessian energy estimate.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.exists_innerHalf_hasWeakHessianOn_harmonic_same_values {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (h : WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) : ∃ (uS : H1Function (scaledOpenCubeSet Q (1 / 2))), uS.toFun = u.toFun ∧ uS.grad = u.grad ∧ Nonempty (HasWeakHessianOn (scaledOpenCubeSet Q (1 / 2)) uS)

The fixed-radius construction can be run after mean-zero normalization and then translated back to the original value representative on the inner cube.

theorem HCPolySupport.CubeCalderonZygmund.exists_harmonic_innerHalf_hessian_energy_bound (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : TriadicCube d) (u : H1Function (openCubeSet Q)), (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → ∃ (uS : H1Function (scaledOpenCubeSet Q (1 / 2))), uS.toFun = u.toFun ∧ uS.grad = u.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q (1 / 2)) uS), H.hessianCoordL2NormSum ≤ C * (cubeScaleFactor Q)⁻¹ * u.gradientCoordL2NormSum

Dimension-only, scale-correct interior Hessian energy estimate for weakly harmonic functions. The construction is run on the mean-zero representative to control the cutoff lower-order term, then its value carrier is translated back by the original cube average.