High-contrast homogenization: Provider.Quenched.SmallContrastSharpLineAtJb

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

The recursion line stated at its own base index

The original sharp line takes hjb : 3 * n / 4 ≤ jb and uses antitonicity to deduce F jb ≤ F (3 * n / 4); its conclusion is then stated at the weaker index 3 * n / 4 and jb disappears. That is exactly right when the iteration runs from the origin, and exactly wrong when it runs from an offset: a proportional index measured from the origin lags out of the shifted clock, and no offset makes the two compatible.

Here each declaration concludes at F jb, the recurrence's chosen base index, and asks instead the one fact the quadratic step really needs, jb ≤ n, which the one-step family already supplies as the upper half of t - Hw ≤ jb ≤ t.

At jb = 3 * n / 4, these statements specialize to the three-quarter-index forms because 3 * n / 4 ≤ n.

The base index may then lag inside the shifted clock,

jb n  :=  n₀ + 3 * (n - n₀) / 4 ,

whose three admissibility facts are proved at the end of the file: it dominates 3 * n / 4, it is bounded by n, and after the shift it is the free index 3 * j / 4, which satisfies the iteration lemma's j ≤ 2 * l' j + 1 at every j.

The scalar step, at the base index

theorem HCPolySupport.HighContrast.Quenched.hrec_of_one_step_sharp_at_jb {F : ℕ → ℝ} (hFnn : ∀ (j : ℕ), 0 ≤ F j) (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) {n H jb : ℕ} (hH : H + 1 ≤ n) (hjbn : jb ≤ n) {a bq cw : ℝ} (ha : 0 ≤ a) (hbq0 : 0 ≤ bq) (hcw : 0 ≤ cw) {W u v w cdrop : ℝ} (hW0 : 0 ≤ W) (hstep : F n ≤ a * (F (n - H) - F n) + bq * F n ^ 2 + cw * W ^ 2) (hWsplit : W ≤ u + v * F jb + w) (hwsq : w ^ 2 ≤ cdrop * iterationDropSum r F n) : F n ≤ (a * (r ^ H)⁻¹ + 3 * cw * cdrop) * iterationDropSum r F n + (bq + 3 * cw * v ^ 2) * F jb ^ 2 + 3 * cw * u ^ 2

hrec_of_one_step_sharp_at_jb with the quadratic slot left at jb.

The isotropy line, at the base index

The shifted base index, and its three admissibility facts