Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.QuantitativeEffectiveScale

High-contrast homogenization: Provider.PolynomialHomogenization.QuantitativeEffectiveScale #

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

One effective scale for a quantitative normalized reference certificate #

The rate prefactor retained by the quantitative certificate is absorbed into one deterministic enlargement of the random source scale. The resulting scale is measurable, is no smaller than the source scale, and carries the same family, order, and decay exponent with unit amplitude.

source
noncomputable def HCPolySupport.HighContrast.amplitudeReductionFactor (amplitude target : ℝ) :
ℝ

The deterministic prefactor needed to reduce a retained amplitude to a positive target amplitude.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.targetedQuantitativeEffectiveScale {d : ℕ} (amplitude target kappa : ℝ) (X : CoeffSpace d → ℝ) :
    CoeffSpace d → ℝ

    One law-level enlargement that reduces the retained pointwise amplitude to a prescribed positive target.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.one_le_amplitudeReductionFactor (amplitude target : ℝ) :
      1 ≤ amplitudeReductionFactor amplitude target
      source
      theorem HCPolySupport.HighContrast.amplitude_le_target_mul_amplitudeReductionFactor {amplitude target : ℝ} (hTarget : 0 < target) :
      amplitude ≤ target * amplitudeReductionFactor amplitude target
      source
      theorem HCPolySupport.HighContrast.QuantitativeNormalizedReferenceCertificate.targetedEffectiveScale {d : ℕ} [NeZero d] {abar : Mat d} {s amplitude target kappa : ℝ} {X : CoeffSpace d → ℝ} {a : CoeffSpace d} (h : QuantitativeNormalizedReferenceCertificate abar s amplitude kappa (X a) a) (hTarget : 0 < target) :
      QuantitativeNormalizedReferenceCertificate abar s target kappa (targetedQuantitativeEffectiveScale amplitude target kappa X a) a

      A quantitative certificate can be rebased once to any positive target amplitude, without changing its family, order, or decay exponent.

      source
      theorem HCPolySupport.HighContrast.QuantitativeNormalizedReferenceCertificate.powerLossRandomScale {d : ℕ} [NeZero d] {abar : Mat d} {s amplitude kappa : ℝ} {X : CoeffSpace d → ℝ} {a : CoeffSpace d} (h : QuantitativeNormalizedReferenceCertificate abar s amplitude kappa (X a) a) (hAmplitude : 1 ≤ amplitude) :
      QuantitativeNormalizedReferenceCertificate abar s 1 kappa (HighContrast.powerLossRandomScale amplitude kappa X a) a

      Absorbing the retained amplitude into the source scale preserves the quantitative certificate and normalizes its pointwise prefactor to one.