Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CommonQuantitativeAffineScale

High-contrast homogenization: Provider.Regularity.CommonQuantitativeAffineScale #

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

The common quantitative affine effective scale #

This module composes the rate-bearing quantitative enlargement with the single rounded-affine multiplier. Keeping this composition named prevents either deterministic loss from being inserted a second time.

source
noncomputable def HCPolySupport.HighContrast.commonQuantitativeAffineScale {d : ℕ} (amplitude target kappaRate Caff overlinePi kappaCube : ℝ) (X : CoeffSpace d → ℝ) :
CoeffSpace d → ℝ

The common effective scale: first absorb the quantitative rate amplitude, then insert the rounded-affine multiplier exactly once.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.le_commonQuantitativeAffineScale {d : ℕ} {amplitude target kappaRate Caff overlinePi kappaCube : ℝ} {X : CoeffSpace d → ℝ} {a : CoeffSpace d} (hkappaRate : 0 < kappaRate) (hX : 0 ≤ X a) :
    X a ≤ commonQuantitativeAffineScale amplitude target kappaRate Caff overlinePi kappaCube X a

    Under a positive rate exponent, the common scale does not decrease a nonnegative raw scale.

    source
    theorem HCPolySupport.HighContrast.one_le_commonQuantitativeAffineScale {d : ℕ} {amplitude target kappaRate Caff overlinePi kappaCube : ℝ} {X : CoeffSpace d → ℝ} {a : CoeffSpace d} (hkappaRate : 0 < kappaRate) (hX : 1 ≤ X a) :
    1 ≤ commonQuantitativeAffineScale amplitude target kappaRate Caff overlinePi kappaCube X a

    A pointwise unit lower bound survives the common enlargement.