Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.HarmonicNormalized

High-contrast homogenization: Provider.Regularity.HarmonicNormalized #

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

Normalized harmonic estimates on Euclidean cubes #

These lemmas convert an unnormalized interior energy estimate to normalized cube L² notation and turn the local Poincare estimate into an affine error bound with the cube-average intercept.

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

The raw central-child Caccioppoli estimate in normalized L² notation, using the Euclidean magnitude of the stored weak gradient.

source
theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_cubeAverage_le_euclideanGradient {d : ℕ} (Q : TriadicCube d) (h : Vec d → ℝ) (c : ℝ) (e : Vec d) (v : H1Function (openCubeSet Q)) (hv : v.toFun = fun (x : Vec d) => h x - (c + vecDot e x)) :
normalizedAffineCandidateError Q h (c + cubeAverage Q v.toFun) e ≤ cubeBesovW12LocalPoincareConstant d * cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (v.grad x)

Choosing the residual cube average as the intercept correction turns the normalized affine error into an oscillation controlled by the Euclidean gradient magnitude.