High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PrintOrderLipschitzScaleComparison

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

Comparing the printed-order and root response scales

The printed-order recurrence and the root certificate differ only in their dimension-and-order response constants. The deterministic factor below absorbs that difference before the coefficient law, matrix, and sample are chosen.

noncomputable def HCPolySupport.HighContrast.Root.printOrderToBaseResponseScaleFactor (d : ℕ) (g kappa : ℝ) : ℝ

The law-free multiplier comparing the printed-order response constant to the base response constant at rate kappa.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Root.one_le_printOrderToBaseResponseScaleFactor (d : ℕ) (g kappa : ℝ) : 1 ≤ printOrderToBaseResponseScaleFactor d g kappa

theorem HCPolySupport.HighContrast.Root.roundedAffineMultiplier_printOrder_le_factor_mul_base (d : ℕ) {g kappa overlinePi : ℝ} (hg : g ∈ Set.Ico 0 1) : roundedAffineMultiplier (printOrderRoundedResponseAffineConstant d g) overlinePi kappa ≤ printOrderToBaseResponseScaleFactor d g kappa * roundedAffineMultiplier (Transport.roundedOuterResponseAffineConstant d) overlinePi kappa

The printed-order affine multiplier is bounded by a law-free factor times the base-response multiplier. The matrix condition number cancels from the comparison.

theorem HCPolySupport.HighContrast.Root.printOrderCommonScale_le_factor_mul_baseCommonScale {d : ℕ} {g sourceAmplitude target kappa : ℝ} {abar : Mat d} {X : CoeffSpace d → ℝ} {a : CoeffSpace d} (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappa) (hX : 1 ≤ X a) : printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a ≤ printOrderToBaseResponseScaleFactor d g kappa * commonQuantitativeAffineScale sourceAmplitude target kappa (Transport.roundedOuterResponseAffineConstant d) (specBound (symmPart abar) * specBound (symmPart abar)⁻¹) kappa X a

At every sample with a unit-lower-bounded source scale, the printed-order common scale is at most a law-free multiple of the root common scale.

theorem HCPolySupport.HighContrast.Root.PrintOrderDecoupledFiniteTerminalSurface.printOrderScale_le_factor_mul_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) : printOrderCommonQuantitativeAffineScale d g surface.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar surface.X a ≤ printOrderToBaseResponseScaleFactor d g kappa * x

The recurrence-start scale of a terminal surface lies below a deterministic multiple of the base-response scale exposed by the root.

theorem HCPolySupport.HighContrast.Root.PrintOrderDecoupledFiniteTerminalSurface.printOrderStartIndex_le_rootStart_add_delay {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) : Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g surface.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar surface.X a) ≤ Quenched.triadicCeilingIndex x + Quenched.triadicCeilingIndex (printOrderToBaseResponseScaleFactor d g kappa)

The recurrence-start generation is at most the root-start generation plus one deterministic delay. In particular, the delay is independent of the probability law, homogenized matrix, coefficient sample, and source scale.