High-contrast homogenization: Provider.Quenched.SmallContrastRecursionShape

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

Shaping the small-contrast weak value onto the iteration lemma

The one-step estimate produces, at generation n, a depth-indexed weighted sum of hatted drops

∑_{j ≤ H_w} r^j (F(n-j) - F(n)),

whereas the cited iteration lemma (Prop42Scalar.HistoryIterationDecay.akbook_iteration_decay) consumes a generation-indexed weighted sum of consecutive increments

∑_{k ∈ [1,n]} r^{n-k} (F(k-1) - F(k)).

This file proves the exact conversion between the two (lagged_drop_sum_le), with the geometric constant (1-r)^{-1} and no dependence on the depth H_w — which is what makes the shaping legitimate when the window reaches back to the entry scale. The proof is a one-line induction on a strengthened invariant carrying the tail r^N(1-r)^{-1}G_N; no double-sum exchange is needed.

Two further scalar facts are recorded, both used when the square of the weak value is regrouped:

• sum_weighted_sqrt_sq_le — the Cauchy–Schwarz regroup that turns the rooted drop sum ∑ w_j √(c·D_j) into the linear drop sum ∑ w_j D_j (this is what makes the drops enter the recursion linearly, as HC (4.17) requires);
• sq_add_three_le — the three-term square split of the weak value into its variance, source and centering groups.

The depth-to-generation conversion

theorem HCPolySupport.HighContrast.Quenched.lagged_drop_sum_le {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) {n N : ℕ} (hN : N ≤ n) : ∑ j ∈ Finset.range N, r ^ j * (F (n - j) - F n) ≤ (1 - r)⁻¹ * ∑ k ∈ Finset.Icc 1 n, r ^ (n - k) * (F (k - 1) - F k)

The depth-indexed drop sum is dominated by the generation-indexed increment sum. For a nonincreasing sequence F and a geometric weight r ∈ [0,1),

∑_{j < N} r^j (F(n-j) - F n) ≤ (1-r)^{-1} ∑_{k ∈ [1,n]} r^{n-k}(F(k-1) - F k)

whenever N ≤ n. The right side is exactly the drop-history sum the iteration decay consumes.

theorem HCPolySupport.HighContrast.Quenched.rpow_weight_eq_pow {mu : ℝ} (j : ℕ) : 3 ^ (-mu * ↑j) = (3 ^ (-mu)) ^ j

The real-power weight of the weak value is the natural power of the one-step ratio.

The Cauchy–Schwarz regroup of the rooted drop sum

theorem HCPolySupport.HighContrast.Quenched.sum_weighted_sqrt_sq_le {ι : Type u_1} (s : Finset ι) (w D : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hD : ∀ i ∈ s, 0 ≤ D i) {c : ℝ} (hc : 0 ≤ c) : (∑ i ∈ s, w i * √(c * D i)) ^ 2 ≤ (∑ i ∈ s, w i) * (c * ∑ i ∈ s, w i * D i)

The Cauchy–Schwarz regroup. A weighted sum of square roots of drops squares to a weighted linear sum of the drops, with the total weight as the constant. This is the step that keeps the drops linear in the recursion.

The three-term square split

theorem HCPolySupport.HighContrast.Quenched.sq_add_three_le (a b c : ℝ) : (a + b + c) ^ 2 ≤ 3 * (a ^ 2 + b ^ 2 + c ^ 2)

The three-term square split of the weak value into its variance, source and centering groups.

theorem HCPolySupport.HighContrast.Quenched.sq_sum_le_of_le {ι : Type u_1} (s : Finset ι) (w D : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hD : ∀ i ∈ s, 0 ≤ D i) {delta : ℝ} (hdelta : ∀ i ∈ s, D i ≤ delta) : (∑ i ∈ s, w i * D i) ^ 2 ≤ (delta * ∑ i ∈ s, w i) * ∑ i ∈ s, w i * D i

The square of a weighted linear drop sum is linear in the drop sum once the drops are uniformly small.