High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.RootScalePhysicalLipschitz

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

Finite-prefix absorption for physical Lipschitz estimates

The homothetic volume identity absorbs the bounded interval between the root scale and the printed recurrence start. Above that start, the selected finite terminal supplies the estimate.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_ellipsoid_le_of_le_mul {d : ℕ} (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r R q : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hq : 1 ≤ q) (hRq : R ≤ q * r) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (ellipsoid abar r) F ≤ ENNReal.ofReal (q ^ d) ^ (1 / 2) * weightedGradNorm b (ellipsoid abar R) F

A bounded ratio of positive ellipsoid radii gives a matrix-uniform weighted-norm comparison.

theorem HCPolySupport.HighContrast.Root.PrintOrderDecoupledFiniteTerminalSurface.physicalLipschitz_from_rootScale {d : ℕ} [NeZero d] {g c kappa Cid : ℝ} {abar : Mat d} {a : CoeffSpace d} {x : ℝ} (surface : Certificate.PrintOrderDecoupledFiniteTerminalSurface d g c kappa Cid abar a x) (hg : g ∈ Set.Ico 0 1) : have q := printOrderToBaseResponseScaleFactor d g kappa; have T := ENNReal.ofReal ((ENNReal.ofReal ((12 * √↑d) ^ d) ^ (1 / 2) * ENNReal.ofReal (2 * surface.recurrenceConstant) * ENNReal.ofReal ((1200 * ↑d) ^ d) ^ (1 / 2) + ENNReal.ofReal ((4800 * ↑d * √↑d) ^ d) ^ (1 / 2)).toReal + 1); have P := ENNReal.ofReal (q ^ d) ^ (1 / 2); ∀ (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 → ∀ r ∈ Set.Icc x R, weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) Du ≤ (T + P * T + P) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du

The selected terminal and the finite homothetic prefix control every physical radius above the root scale.