High-contrast homogenization: Provider.Regularity.CorrectorAnchoredMeanGrowth

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

Scale-linear growth of anchored corrector means

This module converts a scale-linear normalized L² oscillation bound into a scale-linear bound for the centered-cube means. The finitely many scales below the oscillation threshold are retained as a fixed prefix.

theorem HCPolySupport.HighContrast.sum_range_three_pow_succ_le (n : ℕ) : ∑ k ∈ Finset.range n, 3 ^ (k + 1) ≤ 3 * 3 ^ n

The shifted geometric sum at triadic scales is bounded by the next triadic scale.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.exists_abs_cubeAverage_le_three_pow_of_oscillation_bound {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 ∧ ∀ (n : ℕ), q₀ ≤ n → |cubeAverage (originCube d ↑n) z.globalValueRepresentative| ≤ C * 3 ^ n

A scale-linear normalized oscillation bound above a threshold gives a 3^n bound for the fixed-unit-normalized outer corrector mean.