Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PowerLossRandomScale

High-contrast homogenization: Provider.Regularity.PowerLossRandomScale #

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

Random effective scales for deterministic power-law losses #

This module applies the route-independent power-loss enlargement pointwise to a measurable random scale and records its exact threshold-event behavior.

source
noncomputable def HCPolySupport.HighContrast.powerLossRandomScale {Omega : Type u_1} (A kappa : ℝ) (X : Omega → ℝ) :
Omega → ℝ

Enlarge a random scale pointwise so a deterministic prefactor A is absorbed into a negative power with exponent kappa.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.le_powerLossRandomScale {Omega : Type u_1} {A kappa : ℝ} {X : Omega → ℝ} (hA : 1 ≤ A) (hkappa : 0 < kappa) {omega : Omega} (hX : 0 ≤ X omega) :
    X omega ≤ powerLossRandomScale A kappa X omega

    A prefactor at least one enlarges every nonnegative sample scale.

    source
    theorem HCPolySupport.HighContrast.one_le_powerLossRandomScale {Omega : Type u_1} {A kappa : ℝ} {X : Omega → ℝ} (hA : 1 ≤ A) (hkappa : 0 < kappa) {omega : Omega} (hX : 1 ≤ X omega) :
    1 ≤ powerLossRandomScale A kappa X omega

    A pointwise unit lower bound is inherited by the power-loss scale.

    source
    theorem HCPolySupport.HighContrast.prefactor_mul_rpow_ratio_eq_rpow_powerLossRandomScale {Omega : Type u_1} {A kappa r : ℝ} {X : Omega → ℝ} {omega : Omega} (hA : 0 < A) (hkappa : 0 < kappa) (hX : 0 < X omega) (hr : 0 < r) :
    A * (r / X omega) ^ (-kappa) = (r / powerLossRandomScale A kappa X omega) ^ (-kappa)

    The deterministic prefactor is absorbed exactly at every sample.