Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.CoupledMixingScaleDecay

High-contrast homogenization: Provider.Quenched.CoupledMixingScaleDecay #

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

Decay from a coupled mixing-scale certificate #

The least triadic generation above a positive scale loses at most one factor of three. Combining that rounding with one nonnegative summand of the bad-row series turns the coupled certificate into all-later decay.

source
noncomputable def HCPolySupport.HighContrast.Quenched.triadicCeilingIndex (x : ℝ) :
ℕ

The first natural triadic generation whose scale is at least x.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.le_pow_triadicCeilingIndex {x : ℝ} (hx : 1 ≤ x) :
    x ≤ 3 ^ triadicCeilingIndex x

    A positive scale at least one is below its triadic ceiling.

    source
    theorem HCPolySupport.HighContrast.Quenched.pow_triadicCeilingIndex_le_three_mul {x : ℝ} (hx : 1 ≤ x) :
    3 ^ triadicCeilingIndex x ≤ 3 * x

    The triadic ceiling is less than three times the original scale.

    source
    theorem HCPolySupport.HighContrast.Quenched.triadicCeilingIndex_le_of_le_pow {x : ℝ} {m : ℕ} (hx : 1 ≤ x) (hxm : x ≤ 3 ^ m) :
    triadicCeilingIndex x ≤ m

    Any natural generation whose triadic scale dominates x lies above the triadic ceiling of x.

    source
    theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.eventually_row_le_scaled_rpow {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {selectedRow : ℕ → Ω → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) {commonScale : Ω → ℝ} (hkappa : 0 < kappa) (hdelta : 0 < delta) (hone : ∀ (ω : Ω), 1 ≤ commonScale ω) (hscale : ∀ (ω : Ω), W.scale ω ≤ commonScale ω) :
    ∀ᵐ (ω : Ω) ∂P, ∀ (m : ℕ), W.normalization * commonScale ω ≤ 3 ^ m → W.row m ω ≤ delta * (3 ^ m / (W.normalization * commonScale ω)) ^ (-kappa)

    The same selected certificate controls every later row relative to any common scale that dominates its mixing scale. The final normalizer pays for the one-generation rounding of the stopping normalizer.