High-contrast homogenization: Provider.Quenched.SmallContrastSharpDrop #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The sharp single-drop bound: hA1 without the geometric slack #
hA1 (HCPoly.Provider.Quenched.SmallContrastRecursionAssembly) demands
a * ((r ^ H)⁻¹ * (1 - r)⁻¹) + 3 * cw * cdrop ≤ A
so the recursion constant A absorbs both 3 ^ (alpha * H) and
(1 - 3 ^ (-alpha))⁻¹ ≈ 1 / (alpha * log 3). The second factor is's
A ≳ 1/alpha, and it is what made hsmall demand deltaRec = O(alpha ^ 5)
instead of AK.Book's O(alpha ^ 2).
The (1 - r)⁻¹ is pure slack. single_drop_le_iteration_sharp obtains the
lagged drop by bounding one term by a whole sum
(Finset.single_le_sum) and then paying lagged_drop_sum_le's geometric
factor for that sum. Bounding the single term directly costs nothing:
writing a i := F (n-i-1) - F (n-i) ≥ 0, the drop telescopes and every weight
in range is at least r ^ H, so
r ^ H * (F (n-H) - F n) = ∑_{i<H} r ^ H * a i ≤ ∑_{i<H} r ^ i * a i
≤ ∑_{i<n} r ^ i * a i = iterationDropSum r F n .
This file proves that, giving
F (n-H) - F n ≤ (r ^ H)⁻¹ * iterationDropSum r F n
with no (1 - r)⁻¹, and re-derives the recursion step from it so that A
carries only (r ^ H)⁻¹. H is a window height, not a rate, so A is then
free of the 1/alpha blow-up.
These are parallel declarations beside the defective
ones, not bounds on them: single_drop_le_iteration_sharp and hrec_final_sharp_at_jb_src are left
untouched, and the _sharp forms sit next to them.
The weight is antitone #
The telescoping and the reindexing #
The sharp single-drop bound #
The lagged drop, without the geometric factor. For a nonincreasing
F and 0 < r < 1,
F (n-H) - F n ≤ (r ^ H)⁻¹ * iterationDropSum r F n.
Compare single_drop_le_iteration_sharp, which carries a spurious (1 - r)⁻¹
because it bounds this single term by the whole depth-indexed sum before
converting.