Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.HarmonicCaccioppoli

High-contrast homogenization: Provider.Regularity.HarmonicCaccioppoli #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

source
theorem HCPolySupport.CubeCalderonZygmund.harmonic_centralChild_gradient_energy_le {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (hu : WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) :
∫ (x : Vec d) in openCubeSet (centralChild Q), vecNormSq (u.grad x) ≤ 4 * (↑d * (quantitativeCubeCutoffGradientConst d / ((3 / 4 - 1 / 2) * cubeRadius Q)) ^ 2) * ∫ (x : Vec d) in openCubeSet Q, u.toFun x ^ 2

The direct squared-cutoff Caccioppoli estimate needed before the harmonic gradient-gain iteration. Its right side is the parent value energy, with the exact cutoff-gradient coefficient left visible.