Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedAffineEffectiveScale

High-contrast homogenization: Provider.Regularity.RoundedAffineEffectiveScale #

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

The affine effective-scale multiplier #

This module records the affine amplitude and places its sharp positive-power absorption factor into one deterministic effective scale.

source
noncomputable def HCPolySupport.HighContrast.roundedAffineLossAmplitude (Caff overlinePi : ℝ) :
ℝ

The sharp rounded-affine amplitude: C_aff(d) * overlinePi^(1/2).

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.roundedAffineMultiplier (Caff overlinePi kappaCube : ℝ) :
    ℝ

    The affine scale multiplier max {1, (C_aff(d) * overlinePi^(1/2))^(1/kappaCube)}.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.roundedAffineEffectiveScale (Caff overlinePi kappaCube X : ℝ) :
      ℝ

      Insert the affine loss once into a pre-existing common scale.

      Equations
      Instances For
        source
        theorem HCPolySupport.HighContrast.one_le_roundedAffineMultiplier (Caff overlinePi kappaCube : ℝ) :
        1 ≤ roundedAffineMultiplier Caff overlinePi kappaCube
        source
        theorem HCPolySupport.HighContrast.roundedAffineMultiplier_pos (Caff overlinePi kappaCube : ℝ) :
        0 < roundedAffineMultiplier Caff overlinePi kappaCube
        source
        theorem HCPolySupport.HighContrast.roundedAffineLossAmplitude_le_multiplier_rpow {Caff overlinePi kappaCube : ℝ} (hCaff : 0 < Caff) (hPi : 0 < overlinePi) (hkappa : 0 < kappaCube) :
        roundedAffineLossAmplitude Caff overlinePi ≤ roundedAffineMultiplier Caff overlinePi kappaCube ^ kappaCube

        The multiplier has enough kappaCube-power to absorb the full rounded-affine amplitude.

        source
        theorem HCPolySupport.HighContrast.le_roundedAffineEffectiveScale (Caff overlinePi kappaCube X : ℝ) (hX : 0 ≤ X) :
        X ≤ roundedAffineEffectiveScale Caff overlinePi kappaCube X

        The affine enlargement never decreases a nonnegative source scale.

        source
        theorem HCPolySupport.HighContrast.one_le_roundedAffineEffectiveScale (Caff overlinePi kappaCube X : ℝ) (hX : 1 ≤ X) :
        1 ≤ roundedAffineEffectiveScale Caff overlinePi kappaCube X

        A unit-lower-bounded source scale remains unit-lower-bounded after the single affine enlargement.

        source
        theorem HCPolySupport.HighContrast.Measurable.roundedAffineEffectiveScale {Omega : Type u_1} [MeasurableSpace Omega] (Caff overlinePi kappaCube : ℝ) {X : Omega → ℝ} (hX : Measurable X) :
        Measurable fun (ω : Omega) => HighContrast.roundedAffineEffectiveScale Caff overlinePi kappaCube (X ω)

        Applying the fixed affine multiplier preserves measurability of a random source scale.