High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.SelectedGenerationPhysicalLipschitz

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

Physical Lipschitz transport at a selected rounded generation

The finite recurrence is transported through its selected rounded grid and the scalar skew gauge. The lower radius here is the recurrence start scale; comparison with an earlier exposed root scale is a separate finite-prefix argument.

theorem HCPolySupport.HighContrast.Root.PrintOrderDecoupledFiniteTerminalSurface.physicalLipschitz_from_printStart {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) : have xPrint := printOrderCommonQuantitativeAffineScale d g surface.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar surface.X a; ∀ (R : ℝ), xPrint ≤ 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 xPrint R, weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) Du ≤ 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) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du

A selected finite terminal controls the physical weighted gradient norm on every ellipsoid above its own recurrence start.