High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitTsum

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

The burn split at the level of the row series

The burn split is stated over finite partial sums; adapted_scaled_of_standard's accounting is a tsum over the Whitney rows, so the bridge needs the split in that form. This file supplies it, with the two inputs the filling provides: the total row weight (at most one, by the total relative volume being at most one) and the deep row bound (the paid eccentricity against the volume decay, by Transport.sum_relative_volume_row_le).

The flat band is the rows u ≤ D, where the envelope 3 ^ (g * max (u - D) 0) is exactly one; those are paid for by the total alone, which is why the fixed-level bridge's weakening of 1 to Cd * 𝔢 at u = 0 is the whole defect. The deep rows keep the eccentricity, but only against 3 ^ (-D).

theorem HCPolySupport.HighContrast.Quenched.tsum_burn_split_le {g : ℝ} (hg1 : g < 1) {B : ℝ} (hB : 0 ≤ B) (D : ℕ) {w : ℕ → ℝ} (hw0 : ∀ (u : ℕ), 0 ≤ w u) (hwS : Summable w) (hwsum : ∑' (u : ℕ), w u ≤ 1) (hdeep : ∀ (v : ℕ), w (v + (D + 1)) ≤ B * 3 ^ (-(↑v + ↑D + 1))) (hprod : Summable fun (u : ℕ) => w u * 3 ^ (g * max (↑u - ↑D) 0)) : ∑' (u : ℕ), w u * 3 ^ (g * max (↑u - ↑D) 0) ≤ 1 + B * zetaG g * 3 ^ (-↑D)

The burn split over the row series. w is the row weight and D the burn depth; the geometric constant B survives only against 3 ^ (-D).