Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.RootInterface.CommonScaleFactorBound

High-contrast homogenization: #

Provider.PolynomialHomogenization.RootInterface.CommonScaleFactorBound

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

The common affine scale is a law-free multiple of the fold factor #

PrintOrderRateBearingCommonAffineGoodScale d g c κ abar a x forces

x = commonQuantitativeAffineScale sourceAmplitude target κ Caff overlinePi κ X a

which is M · X a for the multiplier

M = roundedAffineMultiplier Caff overlinePi κ *
      (amplitudeReductionFactor sourceAmplitude target) ^ κ⁻¹.

The certificate therefore does not live at the raw quenched scale X a; it lives at M · X a and above. This module bounds M by a law-free amplitude times a power of the homogenized witness eccentricity, which is the shape the root's polynomial-length clause can pay for.

Both of M's factors carry the eccentricity: the affine multiplier through overlinePi = specBound (symmPart abar) * specBound (symmPart abar)⁻¹, whose square root is the witness eccentricity, and the amplitude reduction through the enclosure generation G, which is bracketed by 1 + 3 · ecc · √d.

The multiplier, named #

source
noncomputable def HCPolySupport.HighContrast.RootInterface.commonAffineMultiplier (d : ℕ) (amplitude target kappaRate : ℝ) (abar : Mat d) :
ℝ

The multiplier inserted between the raw quenched scale and the common affine scale that the rate-bearing certificate is read at.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.RootInterface.one_le_commonAffineMultiplier (d : ℕ) {amplitude target kappaRate : ℝ} (hkappa : 0 < kappaRate) (abar : Mat d) :
    1 ≤ commonAffineMultiplier d amplitude target kappaRate abar
    source
    theorem HCPolySupport.HighContrast.RootInterface.commonAffineMultiplier_pos (d : ℕ) {amplitude target kappaRate : ℝ} (hkappa : 0 < kappaRate) (abar : Mat d) :
    0 < commonAffineMultiplier d amplitude target kappaRate abar
    source
    theorem HCPolySupport.HighContrast.RootInterface.commonQuantitativeAffineScale_eq_multiplier_mul (d : ℕ) (amplitude target kappaRate : ℝ) (abar : Mat d) (X : CoeffSpace d → ℝ) (a : CoeffSpace d) :
    commonQuantitativeAffineScale amplitude target kappaRate (Transport.roundedOuterResponseAffineConstant d) (specBound (symmPart abar) * specBound (symmPart abar)⁻¹) kappaRate X a = commonAffineMultiplier d amplitude target kappaRate abar * X a

    The common affine scale is exactly the multiplier times the raw scale.

    The affine leg #

    source
    theorem HCPolySupport.HighContrast.RootInterface.sqrt_overlinePi_eq_witnessEccentricity {d : ℕ} (abar : Mat d) :
    √(specBound (symmPart abar) * specBound (symmPart abar)⁻¹) = witnessEccentricity (symmPart abar)

    The affine multiplier's own amplitude is the witness eccentricity.

    source
    theorem HCPolySupport.HighContrast.RootInterface.roundedAffineMultiplier_le_fold (d : ℕ) {kappaRate : ℝ} (hkappa : 0 < kappaRate) (abar : Mat d) :
    roundedAffineMultiplier (Transport.roundedOuterResponseAffineConstant d) (specBound (symmPart abar) * specBound (symmPart abar)⁻¹) kappaRate ≤ max 1 (Transport.roundedOuterResponseAffineConstant d ^ kappaRate⁻¹) * RowSupply.eccentricityFoldFactor abar kappaRate⁻¹

    The amplitude leg #

    source
    noncomputable def HCPolySupport.HighContrast.RootInterface.certAmplitudeBase (d : ℕ) (s rho : ℝ) :
    ℝ

    The law-free half of the retained source amplitude.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.RootInterface.certAmplitudeBase_nonneg (d : ℕ) (s rho : ℝ) :
      0 ≤ certAmplitudeBase d s rho
      source
      theorem HCPolySupport.HighContrast.RootInterface.normalizedReferencePowerAmplitude_le_fold {d : ℕ} {abar : Mat d} {s rho delta : ℝ} {G : ℕ} (_hrho : 0 < rho) (hrho1 : rho ≤ 1) (hgap : rho < 2 * s) (hdelta : delta ∈ Set.Ioo 0 1) (hG : 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d)) :
      normalizedReferencePowerAmplitude d s rho delta G ≤ certAmplitudeBase d s rho * RowSupply.eccentricityFoldFactor abar 1

      The retained source amplitude is a law-free constant times one power of the eccentricity fold factor.

      source
      theorem HCPolySupport.HighContrast.RootInterface.amplitudeReductionFactor_rpow_le_fold {d : ℕ} {abar : Mat d} {amplitude target Amp kappaRate : ℝ} (hkappa : 0 < kappaRate) (hAmp : 0 ≤ Amp) (htarget : 0 < target) (hamp : amplitude ≤ Amp * RowSupply.eccentricityFoldFactor abar 1) :
      amplitudeReductionFactor amplitude target ^ kappaRate⁻¹ ≤ max 1 (Amp / target) ^ kappaRate⁻¹ * RowSupply.eccentricityFoldFactor abar kappaRate⁻¹

      The amplitude leg of the multiplier, in fold form.

      The full multiplier bound #

      source
      noncomputable def HCPolySupport.HighContrast.RootInterface.rootCertAmplitude (d : ℕ) (s rho target kappaRate : ℝ) :
      ℝ

      The law-free amplitude of the certificate's own length factor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.HighContrast.RootInterface.one_le_rootCertAmplitude (d : ℕ) {s rho target kappaRate : ℝ} (hkappa : 0 < kappaRate) :
        1 ≤ rootCertAmplitude d s rho target kappaRate
        source
        theorem HCPolySupport.HighContrast.RootInterface.commonAffineMultiplier_le_fold {d : ℕ} {abar : Mat d} {s rho delta target kappaRate : ℝ} {G : ℕ} (hkappa : 0 < kappaRate) (hrho : 0 < rho) (hrho1 : rho ≤ 1) (hgap : rho < 2 * s) (hdelta : delta ∈ Set.Ioo 0 1) (htarget : 0 < target) (hG : 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d)) :
        commonAffineMultiplier d (normalizedReferencePowerAmplitude d s rho delta G) target kappaRate abar ≤ rootCertAmplitude d s rho target kappaRate * RowSupply.eccentricityFoldFactor abar (2 * kappaRate⁻¹)

        The certificate's scale multiplier is a law-free amplitude times two powers of the eccentricity fold factor.