High-contrast homogenization: Provider.Regularity.CorrectorAnchoredMean

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

Fixed-unit normalization of every local corrector representative

The projective carrier stores zero mean only at scale zero. Compatibility of the global representative transports that normalization to the restriction of every larger canonical local H¹ representative. This is the anchor for the successive-cube mean telescope used in the Liouville growth argument.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.cubeAverage_globalValueRepresentative_eq_localH1Function {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) : cubeAverage (originCube d ↑n) z.globalValueRepresentative = cubeAverage (originCube d ↑n) (z.localH1Function n).toFun

The global scalar representative and the canonical local H¹ representative have the same average on every exhaustion cube.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.cubeAverage_localH1Function_eq_of_le {d m n : ℕ} (z : NormalizedLocalH1Carrier d) (hmn : m ≤ n) : cubeAverage (originCube d ↑m) (z.localH1Function n).toFun = cubeAverage (originCube d ↑m) (z.localH1Function m).toFun

A larger canonical local representative has the same average on every smaller exhaustion cube as the smaller canonical representative.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.cubeAverage_globalValueRepresentative_zero {d : ℕ} (z : NormalizedLocalH1Carrier d) : cubeAverage (originCube d 0) z.globalValueRepresentative = 0

The global representative has zero average on the unit origin cube.