High-contrast homogenization: Provider.Window.BurnSeries

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

Rounded-grid and burn-series bounds

The inverse of a rounded grid is uniformly bounded. The Whitney decay and the source burn discount combine into the geometric series defining zetaG.

theorem HCPolySupport.HighContrast.Window.norm_inv_roundedGrid_le {d : ℕ} {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) : ‖(roundedGrid l m)⁻¹‖ ≤ 101 / 100

The inverse spectral norm of a rounded grid is at most 101 / 100.

theorem HCPolySupport.HighContrast.Window.burnDiscount_sub_nat_le {g : ℝ} (hg : 0 ≤ g) (jStar r : ℤ) (u : ℕ) : burnDiscount g jStar (r - ↑u) ≤ burnDiscount g jStar r * 3 ^ (g * ↑u)

Lowering the cell scale by u increases the burn discount by at most 3^(g u).

theorem HCPolySupport.HighContrast.Window.summable_zpow_mul_burnDiscount_and_tsum_le {g : ℝ} (hg : g ∈ Set.Ico 0 1) (jStar r : ℤ) : (Summable fun (u : ℕ) => 3 ^ (-↑u) * burnDiscount g jStar (r - ↑u)) ∧ ∑' (u : ℕ), 3 ^ (-↑u) * burnDiscount g jStar (r - ↑u) ≤ zetaG g * burnDiscount g jStar r

The Whitney factor and burn discount have the zetaG total printed in the source-window estimate.