High-contrast homogenization: Provider.PolynomialHomogenization.BoundaryRowShift

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

Shifting a geometric boundary row

Enlarging the containing cube shifts the spatial excess row by a fixed number of generations. The sharper boundary kernel is summable against any nonnegative row controlled by the shifted fractional kernel.

theorem HCPolySupport.HighContrast.summable_boundary_row_and_tsum_le_shifted_row {rho : ℝ} (hrho1 : rho ≤ 1) (G : ℕ) (k : ℤ) (B : ℤ → ℝ) (hB0 : ∀ (r : ℤ), 0 ≤ B r) (hrow : Summable fun (n : ℕ) => 3 ^ (-rho * ↑n) * B (k + ↑G - ↑n)) : (Summable fun (n : ℕ) => 3 ^ (-↑n) * B (k - ↑n)) ∧ ∑' (n : ℕ), 3 ^ (-↑n) * B (k - ↑n) ≤ 3 ^ (rho * ↑G) * ∑' (n : ℕ), 3 ^ (-rho * ↑n) * B (k + ↑G - ↑n)

A shifted fractional row controls the sharper integer boundary row. The fixed shift appears only as its geometric prefactor.