Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.PrintOrderCertificateInhabitation

High-contrast homogenization: Provider.PolynomialHomogenization.PrintOrderCertificateInhabitation #

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

Printed-order certificate inhabitation #

The row-to-reference comparison is kept at the original measurable scale. Its deterministic enclosure and exponent-gap prefactor is retained in the amplitude. Taking the square root then gives exactly the halved row-decay rate used by the printed reconstruction.

source
noncomputable def HCPolySupport.HighContrast.normalizedReferencePowerPrefactor (d : ℕ) (s rho : ℝ) (G : ℕ) :
ℝ

The deterministic coefficient multiplying the squared physical row in the normalized-reference comparison at one fixed enclosure shift.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.normalizedReferencePowerAmplitude (d : ℕ) (s rho delta : ℝ) (G : ℕ) :
    ℝ

    The square-root amplitude retained from the physical block-row bound.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.exists_normalizedReferencePowerTail_of_hasAllLaterPhysicalBlockRow {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s rho kappa delta : ℝ) (S X : CoeffSpace d → ℝ) (G : ℕ) (hG : witnessEccentricity (symmPart abar) * √↑d ≤ 3 ^ ↑G) (hrho : 0 < rho) (hrho1 : rho ≤ 1) (hrhoGap : rho < 2 * s) (hkappa : 0 < kappa) (hdelta : 0 ≤ delta) (hrow : Quenched.HasAllLaterPhysicalBlockRow rho kappa delta (Book.Ch02.constantBlockMatrix abar) S X a) (hXone : 1 ≤ X a) (hburn : S a ≤ X a) :
      ∃ (aRef : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) ∧ ScalarIdentityPowerTail aRef s (normalizedReferencePowerAmplitude d s rho delta G) (kappa / 2) (X a)

      A physical block row produces one global exactly normalized reference family whose identity weak errors retain the square-root amplitude and the halved row-decay rate at the original real scale.