High-contrast homogenization: Provider.Regularity.CorrectorAffineCubeGrowth

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

Affine-plus-corrector cube growth

The forward Liouville inclusion concerns an affine function plus its anchored corrector and an arbitrary constant. This module adds the elementary affine and constant pieces to the correction-only cube-growth estimate.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.exists_affineAdd_cubeLpNorm_le_three_pow {d : ℕ} (z : NormalizedLocalH1Carrier d) (q₀ : ℕ) (C : ℝ) (hC : 0 ≤ C) (hcube : ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 z.globalValueRepresentative ≤ C * 3 ^ q) (e : Vec d) (c : ℝ) : ∃ (Cfull : ℝ), 0 ≤ Cfull ∧ ∀ (q : ℕ), q₀ ≤ q → (cubeLpNorm (originCube d ↑q) 2 fun (x : Vec d) => vecDot e x + z.globalValueRepresentative x + c) ≤ Cfull * 3 ^ q

Adding an affine function and a constant preserves scale-linear centered-cube growth.