High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1FinitePrefixAbsorption

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

Finite-prefix absorption for physical C1 estimates

A simultaneous-slope estimate beginning at a bounded larger radius extends to the original radius. On the finite prefix, normalized energy monotonicity and homothetic ellipsoid volume scaling supply the missing bound.

theorem HCPolySupport.HighContrast.Root.exists_rangeCompletePhysicalC1_of_boundedStart {d : ℕ} (L : ℕ) (eta A : ℝ) (heta : 0 ≤ eta) (hA : 0 < A) : ∃ (K : ℝ), 0 < K ∧ ∀ (abar : Mat d), Matrix.PosDef (symmPart abar) → ∀ (a : CoeffSpace d) (x : ℝ), 1 ≤ x → ∀ (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), (∀ (c : ℝ) (e e' : Vec d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (y : Vec d) => c • gradPhi e a y + gradPhi e' a y) → ∀ (R : ℝ), x ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), MemH1a (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) u Du → IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du → (have rStart := 3 ^ (Quenched.triadicCeilingIndex x + L); rStart ≤ R → ∃ (e : Vec d), ∀ r ∈ Set.Icc rStart R, (weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) fun (y : Vec d) => Du y - (e + gradPhi e a y)) ≤ ENNReal.ofReal (A * (r / R) ^ eta) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du) → ∃ (e : Vec d), ∀ r ∈ Set.Icc x R, (weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) fun (y : Vec d) => Du y - (e + gradPhi e a y)) ≤ ENNReal.ofReal (K * (r / R) ^ eta) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du

A delayed physical C1 estimate extends through a bounded homothetic prefix. The same slope is retained whenever the delayed range is nonempty; when the whole interval lies in the prefix, the zero slope is used.