Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.Prop42Scalar.CorrectedTiltTransfer

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

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

Corrected adapted-to-Euclidean scale transfer #

The intermediate adapted scale is chosen as m / 2 + n₀. The resulting parity loss is made explicit and absorbed into a fixed prefactor. All results are scalar and independent of the probability carrier.

source
def HCPolySupport.HighContrast.Quenched.Prop42Scalar.correctedTiltScale (n₀ m : ℕ) :
ℕ

The intermediate scale for an outer Euclidean generation.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.correctedTiltScale_admissible {n₀ m : ℕ} (hm : 2 * n₀ ≤ m) :
    2 * n₀ ≤ correctedTiltScale n₀ m ∧ 2 * (correctedTiltScale n₀ m - n₀) ≤ m

    The corrected intermediate scale satisfies both side conditions of the adapted-to-Euclidean comparison.

    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.outer_sub_two_mul_le_two_mul_correctedTiltScale_sub_add_one {n₀ m : ℕ} (hm : 2 * n₀ ≤ m) :
    m - 2 * n₀ ≤ 2 * (correctedTiltScale n₀ m - 2 * n₀) + 1

    The parity defect in the adapted decay is at most one generation.

    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.outer_sub_two_mul_le_two_mul_outer_sub_correctedTiltScale {n₀ m : ℕ} (hm : 2 * n₀ ≤ m) :
    m - 2 * n₀ ≤ 2 * (m - correctedTiltScale n₀ m)

    The Euclidean comparison gap is at least half of the post-entry outer generation.

    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.correctedTiltScale_decay_le {κ : ℝ} (hκ : 0 ≤ κ) {n₀ m : ℕ} (hm : 2 * n₀ ≤ m) :
    Real.rpow 3 (-κ * ↑(correctedTiltScale n₀ m - 2 * n₀)) ≤ Real.rpow 3 (κ / 2) * Real.rpow 3 (-κ / 2 * ↑(m - 2 * n₀))

    The hatted decay at the corrected intermediate scale loses only the fixed parity factor 3^(κ/2) relative to the outer rate κ/2.

    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.correctedTiltScale_error_decay_le {κ : ℝ} (hκ_one : κ ≤ 1) {n₀ m : ℕ} (hm : 2 * n₀ ≤ m) :
    Real.rpow 3 (-↑(m - correctedTiltScale n₀ m)) ≤ Real.rpow 3 (-κ / 2 * ↑(m - 2 * n₀))

    If κ ≤ 1, the Euclidean comparison error decays at least as fast as the outer rate κ/2.

    source
    theorem HCPolySupport.HighContrast.Quenched.Prop42Scalar.corrected_tilt_transfer {F Fhat : ℕ → ℝ} {A κ : ℝ} (hA : 0 ≤ A) (hκ : 0 ≤ κ) (hκ_one : κ ≤ 1) {n₀ m : ℕ} (hm : 2 * n₀ ≤ m) (hhat : Fhat (correctedTiltScale n₀ m) ≤ A * Real.rpow 3 (-κ * ↑(correctedTiltScale n₀ m - 2 * n₀))) (htransfer : F m ≤ Fhat (correctedTiltScale n₀ m) + A * Real.rpow 3 (-↑(m - correctedTiltScale n₀ m))) :
    F m ≤ A * (Real.rpow 3 (κ / 2) + 1) * Real.rpow 3 (-κ / 2 * ↑(m - 2 * n₀))

    Scalar transfer from an adapted decay and a Euclidean comparison error to the corrected outer decay.