High-contrast homogenization: Provider.Regularity.CorrectorAnchoredFunctionGrowth

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

Scale-linear centered-cube growth of anchored correctors

The normalized L² norm is split into its fluctuation and mean. The oscillation is supplied by the caller, while the anchored telescope controls the mean.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.exists_globalRepresentativeLpBound_of_oscillation {d : ℕ} (z : NormalizedLocalH1Carrier d) (q₀ : ℕ) (M : ℝ) (hM : 0 ≤ M) (hosc : ∀ (q : ℕ), q₀ ≤ q → cubeBesovOscillation (originCube d ↑q) 2 (z.localH1Function q).toFun ≤ M * 3 ^ q) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 z.globalValueRepresentative ≤ C * 3 ^ q

A scale-linear normalized oscillation bound above a threshold gives a scale-linear normalized L² bound for the global value representative on the centered exhaustion cubes.