High-contrast homogenization: Provider.Quenched.SmallContrastDropRegroup

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

The drop slots of the weak value against the iteration sum

The two depth sums of weakValueSharpMajorant_le_three_group_summed_at_level that carry the hatted mean drops are

∑_{j ≤ H_w} 3^{-μ j} · Dr j (the linear slot of the per-scale budget)

and

∑_{j ≤ H_w} 3^{-ν j} · √(2d · Dr j) (the rooted slot).

Both are converted here into the drop-history sum

T_n = ∑_{k ∈ [1,n]} (3^{-μ})^{n-k} (F(k-1) - F(k))

that the iteration decay consumes, using the mean-drop carrier's own shape Dr j ≤ c_D (F(n-j) - F(n)) (meanDrop2ValueIsotropy is exactly 4d times that drop times reference constants). The rooted slot is first regrouped by Cauchy–Schwarz, which is what keeps the drops linear in the recursion — the printed mechanism of HC (4.17).

theorem HCPolySupport.HighContrast.Quenched.geom_sum_le_inv_one_sub {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (M : ℕ) : ∑ j ∈ Finset.range M, r ^ j ≤ (1 - r)⁻¹

A geometric series is below the inverse of its gap.

theorem HCPolySupport.HighContrast.Quenched.iteration_sum_nonneg {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {r : ℝ} (hr0 : 0 ≤ r) (n : ℕ) : 0 ≤ ∑ k ∈ Finset.Icc 1 n, r ^ (n - k) * (F (k - 1) - F k)

The drop-history sum of the iteration lemma is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.weak_drop_sum_le_iteration {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {mu : ℝ} (hmu : 0 < mu) {n Hw : ℕ} (hHw : Hw + 1 ≤ n) {cD : ℝ} (hcD0 : 0 ≤ cD) {Dr : ℕ → ℝ} (hDr : ∀ j ∈ Finset.range (Hw + 1), Dr j ≤ cD * (F (n - j) - F n)) : ∑ j ∈ Finset.range (Hw + 1), 3 ^ (-mu * ↑j) * Dr j ≤ cD * ((1 - 3 ^ (-mu))⁻¹ * ∑ k ∈ Finset.Icc 1 n, (3 ^ (-mu)) ^ (n - k) * (F (k - 1) - F k))

The linear drop slot against the iteration sum.

theorem HCPolySupport.HighContrast.Quenched.weak_rooted_drop_sum_sq_le {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {nu : ℝ} (hnu : 0 < nu) {n Hw : ℕ} (hHw : Hw + 1 ≤ n) {c cD : ℝ} (hc : 0 ≤ c) (hcD0 : 0 ≤ cD) {Dr : ℕ → ℝ} (hDr0 : ∀ (j : ℕ), 0 ≤ Dr j) (hDr : ∀ j ∈ Finset.range (Hw + 1), Dr j ≤ cD * (F (n - j) - F n)) : (∑ j ∈ Finset.range (Hw + 1), 3 ^ (-nu * ↑j) * √(c * Dr j)) ^ 2 ≤ (1 - 3 ^ (-nu))⁻¹ * (c * (cD * ((1 - 3 ^ (-nu))⁻¹ * ∑ k ∈ Finset.Icc 1 n, (3 ^ (-nu)) ^ (n - k) * (F (k - 1) - F k))))

The rooted drop slot against the iteration sum. The Cauchy–Schwarz regroup turns the square of the rooted sum into a linear multiple of the drop-history sum.