High-contrast homogenization: Provider.Quenched.Prop42Scalar.CorrectedTiltEndpoint #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Scalar endpoint for the corrected tilt transfer #
This file composes the halfway scale choice with prefactor absorption and polynomial delay accounting. The only inputs are an adapted tail, its Euclidean comparison, and scalar power bounds.
theorem
HCPolySupport.HighContrast.Quenched.Prop42Scalar.exists_power_bounded_unit_decay_of_corrected_tilt
{F Fhat : ℕ → ℝ}
{A κ base Centry Cpref : ℝ}
(hA : 0 ≤ A)
(hκ : 0 < κ)
(hκ_one : κ ≤ 1)
(hbase : 3 ≤ base)
(hCpref : 0 ≤ Cpref)
{n₀ : ℕ}
(hentry : 3 ^ (2 * n₀) ≤ base.rpow Centry)
(hpref : A * (Real.rpow 3 (κ / 2) + 1) ≤ base.rpow Cpref)
(hhat : ∀ (n : ℕ), 2 * n₀ ≤ n → Fhat n ≤ A * Real.rpow 3 (-κ * ↑(n - 2 * n₀)))
(htransfer :
∀ (m : ℕ), 2 * n₀ ≤ m → F m ≤ Fhat (correctedTiltScale n₀ m) + A * Real.rpow 3 (-↑(m - correctedTiltScale n₀ m)))
:
An adapted tail and its corrected halfway transfer yield a unit-prefactor Euclidean tail after a power-bounded delay.