High-contrast homogenization: Provider.Regularity.HarmonicCaccioppoliNorm #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.CubeCalderonZygmund.exists_harmonic_centralChild_euclideanGradient_cubeLpNorm_le
(d : ℕ)
:
∃ (C : ℝ),
0 < C ∧ ∀ (Q : TriadicCube d) (u : H1Function (openCubeSet Q)),
(WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) →
(cubeLpNorm (centralChild Q) 2 fun (x : Vec d) => euclideanNorm (u.grad x)) ≤ C * (cubeScaleFactor Q)⁻¹ * cubeLpNorm Q 2 u.toFun
The normalized direct Caccioppoli estimate with all cutoff arithmetic absorbed into one dimension-only constant.