High-contrast homogenization: Provider.Quenched.SmallContrastTwoOffsetEndpointBody #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The hcore body from a decay at any offset #
The endpoint's tail does not care where the geometric decay starts: the offset
joins the prefactor, and the prefactor is what hpref already carries into a
law-free exponent. Stating that once, at a free offset, isolates the route's
one open step.
With this in place the offset route reduces to a single missing lemma — the
two-offset iteration, whose recursion is available only from a second offset
n₀ ≥ ns while the family reports its quadratic index at shiftedBaseIndex ns
(the two-offset admissibility condition). Everything above and below it is
already proved.
theorem
HCPolySupport.HighContrast.Quenched.hcore_body_of_two_offset_decay
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{N₀ n₀ : ℕ}
{Kpre gam : ℝ}
(hgam0 : 0 < gam)
(hgam1 : gam ≤ 1)
(hKpre0 : 0 ≤ Kpre)
(hFnn : ∀ (n : ℕ), 0 ≤ hatExcess P q N₀ n)
(hFmono : ∀ (m n : ℕ), m ≤ n → hatExcess P q N₀ n ≤ hatExcess P q N₀ m)
(hdecay : ∀ (n : ℕ), n₀ ≤ n → hatExcess P q N₀ n ≤ Kpre * (3 ^ (-gam)) ^ (n - n₀))
{base Centry Cpref : ℝ}
(hbase : 3 ≤ base)
(hCpref : 0 ≤ Cpref)
(hentry : 3 ^ (2 * N₀) ≤ base.rpow Centry)
(hpref : 9 / 2 * ((Kpre + hatExcess P q N₀ 0) * 3 ^ (gam * ↑n₀)) * (Real.rpow 3 (gam / 2) + 1) ≤ base.rpow Cpref)
(htransfer :
∀ (m : ℕ),
2 * N₀ ≤ m →
annealedContrast P ↑m - 1 ≤ 9 / 2 * (↑d * (adaptedHattedContrast P q ↑(Prop42Scalar.correctedTiltScale N₀ m) - 1)) + 9 / 2 * ((Kpre + hatExcess P q N₀ 0) * 3 ^ (gam * ↑n₀)) * Real.rpow 3 (-↑(m - Prop42Scalar.correctedTiltScale N₀ m)))
:
The hcore body from a decay at any offset.