High-contrast homogenization: Provider.Response.DiagonalWeakNormSummation

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

Scale summation for the diagonal weak estimate

The estimates here perform the geometric summations of the weak-norm bound on the bad event and of the contribution of the old scales. They are stated separately from the variational estimates so that the extended-real seminorm is converted from scale-by-scale bounds only after summability has been established.

From scale bounds to the extended-real seminorm

theorem HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_le_of_summable {d : ℕ} {q : Mat d} {t : ℤ} {s : ℝ} {F : Vec d → BlockVec d} {b : ℕ → ℝ} (hb0 : ∀ (j : ℕ), 0 ≤ b j) (hbsum : Summable b) (hscale : ∀ (j : ℕ), (3 ^ (-(s * ↑j)) * blockAvsumL2 (alignedIndex q (t - ↑j) t) fun (z : Fin d → ℤ) => blockCellAverage (adaptedCellAt q (t - ↑j) z) F) ≤ b j) : ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s F ≤ ENNReal.ofReal (∑' (j : ℕ), b j)

A summable real majorant for the normalized scale terms bounds the extended-real weak seminorm by the image of its real sum.

The bad branch

theorem HCPolySupport.HighContrast.Response.tsum_diagonalWeak_bad_majorant_le {s rho delta M : ℝ} (hrho : 0 < rho) (hs : rho / 2 < s) (hs1 : s ≤ 1) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (hbad : delta < M) : ∑' (j : ℕ), (3 ^ (-(s * ↑j)) + √M * 3 ^ (-((s - rho / 2) * ↑j))) ≤ 8 * (√delta)⁻¹ / (2 * s - rho) * √M

The two geometric rows in the all-scale estimate have the printed bad branch bound. The harmless numerical factor eight is absorbed by the dimension-only constant in the final lemma.

The good old-scale branch

theorem HCPolySupport.HighContrast.Response.tsum_diagonalWeak_good_tail_majorant_le {s rho delta M : ℝ} (hrho : 0 < rho) (hs : rho / 2 < s) (hs1 : s ≤ 1) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (hgood : M ≤ delta) (n : ℕ) : ∑' (j : ℕ), (3 ^ (-(s * (↑j + ↑n))) + √M * 3 ^ (-((s - rho / 2) * (↑j + ↑n)))) ≤ 8 * (√delta)⁻¹ / (2 * s - rho) * 3 ^ (-((s - rho / 2) * ↑n))

The tail of the two scale-energy rows has the printed good-branch decay. The shift n is the number of scales omitted from the recent window.

The released split level

theorem HCPolySupport.HighContrast.Response.tsum_diagonalWeak_bad_majorant_at_level_le {s rho delta M : ℝ} (hrho : 0 < rho) (hs : rho / 2 < s) (hs1 : s ≤ 1) (hdelta : 0 < delta) (hbad : delta < M) : ∑' (j : ℕ), (3 ^ (-(s * ↑j)) + √M * 3 ^ (-((s - rho / 2) * ↑j))) ≤ 4 * (1 + √delta) * (√delta)⁻¹ / (2 * s - rho) * √M

The bad branch at a released split level.

theorem HCPolySupport.HighContrast.Response.tsum_diagonalWeak_good_tail_majorant_at_level_le {s rho delta M : ℝ} (hrho : 0 < rho) (hs : rho / 2 < s) (hs1 : s ≤ 1) (hgood : M ≤ delta) (n : ℕ) : ∑' (j : ℕ), (3 ^ (-(s * (↑j + ↑n))) + √M * 3 ^ (-((s - rho / 2) * (↑j + ↑n)))) ≤ 4 * (1 + √delta) / (2 * s - rho) * 3 ^ (-((s - rho / 2) * ↑n))

The good old-scale tail at a released split level.