High-contrast homogenization: Provider.Regularity.RoundedOuterScaleFubini

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

Nonnegative Fubini comparison for the rounded boundary row

The outer q = 2 response weight and the inner codimension-one filling weight form a nonnegative convolution. Regrouping it by total depth exposes the exact gap 1 - 2 * s; a fixed parent shift costs exactly 3 ^ (2 * s * G).

theorem HCPolySupport.HighContrast.Transport.summable_boundaryConvolution_shift_and_tsum_le {s C : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hC : 0 ≤ C) (G : ℕ) (A : ℕ → ℝ) (hA0 : ∀ (n : ℕ), 0 ≤ A n) (hA : Summable fun (n : ℕ) => Book.Ch02.geometricWeight s 2 n * A n) : (∀ (l : ℕ), Summable fun (u : ℕ) => C * 3 ^ (-↑u) * A (G + (l + u))) ∧ (Summable fun (l : ℕ) => Book.Ch02.geometricWeight s 2 l * ∑' (u : ℕ), C * 3 ^ (-↑u) * A (G + (l + u))) ∧ ∑' (l : ℕ), Book.Ch02.geometricWeight s 2 l * ∑' (u : ℕ), C * 3 ^ (-↑u) * A (G + (l + u)) ≤ C * (Book.Ch02.geometricDiscount (1 - 2 * s) 1)⁻¹ * Real.rpow 3 (2 * s * ↑G) * ∑' (n : ℕ), Book.Ch02.geometricWeight s 2 n * A n

The nonnegative outer response row and inner rounded-filling row may be regrouped by total depth. The theorem derives every inner-row summability witness, outer summability, and the exact shifted convolution bound.