Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.Prop42Scalar.DecayDelay

High-contrast homogenization: Provider.Quenched.Prop42Scalar.DecayDelay #

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

Absorbing a decay prefactor into a polynomially bounded delay #

This file turns a geometric tail with a nonnegative prefactor into a unit- prefactor tail after an explicit integer delay. It also shows that this delay has a power bound whenever the prefactor and the pre-existing entry generation have power bounds in the same base.

source
noncomputable def HCPolySupport.HighContrast.Quenched.Prop42Scalar.prefactorDelay (A α : ℝ) :
ℕ

The extra integer delay needed to absorb a nonnegative prefactor into a decay of rate α.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.prefactor_le_three_rpow_alpha_mul_prefactorDelay {A α : ℝ} (hα : 0 < α) :
    A ≤ Real.rpow 3 (α * ↑(prefactorDelay A α))

    The defining delay makes the prefactor no larger than the recovered positive exponential factor.

    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.prefactor_mul_decay_add_prefactorDelay_le {A α : ℝ} (hα : 0 < α) (j : ℕ) :
    A * Real.rpow 3 (-α * ↑(prefactorDelay A α + j)) ≤ Real.rpow 3 (-α * ↑j)

    After adding prefactorDelay, the geometric tail has unit prefactor.

    source
    noncomputable def HCPolySupport.HighContrast.Quenched.Prop42Scalar.totalDecayDelay (n₀ : ℕ) (A α : ℝ) :
    ℕ

    The full delay combines a pre-existing entry generation with the extra prefactor-absorption delay.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.unit_prefactor_decay_after_totalDecayDelay {F : ℕ → ℝ} {A α : ℝ} (hα : 0 < α) {n₀ : ℕ} (hF : ∀ (n : ℕ), 2 * n₀ ≤ n → F n ≤ A * Real.rpow 3 (-α * ↑(n - 2 * n₀))) (j : ℕ) :
      F (totalDecayDelay n₀ A α + j) ≤ Real.rpow 3 (-α * ↑j)

      A post-entry geometric bound becomes a unit-prefactor bound after the full delay.

      source
      theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.prefactorDelay_cast_le_logb {A α base C : ℝ} (hα : 0 < α) (hbase : 3 ≤ base) (hC : 0 ≤ C) (hA : A ≤ base.rpow C) :
      ↑(prefactorDelay A α) ≤ (1 + C / α) * Real.logb 3 base

      If the prefactor is bounded by a power of a base at least three, then its absorption delay is bounded by a fixed multiple of the base-three logarithm.

      source
      theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.three_pow_prefactorDelay_le_rpow {A α base C : ℝ} (hα : 0 < α) (hbase : 3 ≤ base) (hC : 0 ≤ C) (hA : A ≤ base.rpow C) :
      3 ^ prefactorDelay A α ≤ base.rpow (1 + C / α)

      Power form of the polynomial bound on the prefactor-absorption delay.

      source
      theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.three_pow_totalDecayDelay_le_rpow {n₀ : ℕ} {A α base Centry Cpref : ℝ} (hα : 0 < α) (hbase : 3 ≤ base) (hCpref : 0 ≤ Cpref) (hentry : 3 ^ (2 * n₀) ≤ base.rpow Centry) (hpref : A ≤ base.rpow Cpref) :
      3 ^ totalDecayDelay n₀ A α ≤ base.rpow (Centry + (1 + Cpref / α))

      Combining a polynomial entry generation with a polynomial prefactor gives a polynomial bound on the full unit-prefactor delay.