High-contrast homogenization: Provider.Regularity.HarmonicHessianNormalized #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.CubeCalderonZygmund.exists_harmonic_centralChild_normalized_hessian_energy_bound
{d : ℕ}
:
∃ (A : ENNReal),
0 < A ∧ A ≠ ⊤ ∧ ∀ (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),
ENNReal.ofReal (cubeScaleFactor (centralChild Q)) * ∑ i : Fin d,
∑ j : Fin d,
MeasureTheory.eLpNorm (fun (x : Vec d) => H.hess i j x) 2
(normalizedCubeMeasure (centralChild Q)) ≤ A * ∑ j : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x j) 2 (normalizedCubeMeasure Q)
A dimension-only normalized Hessian-energy carrier for a harmonic function on the central child of a Euclidean cube.