Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.Series

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Finite-exponent multiscale ellipticity: series identities

theorem HCPolySupport.Book.Ch02.LambdaSqFinite_series_nonneg {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : TriadicCoeffFamily d) (_hq : 0 ≤ q) (hsq : 0 ≤ s * q) : 0 ≤ ∑' (n : ℕ), geometricWeight s q n * (maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)

theorem HCPolySupport.Book.Ch02.lambdaSqFinite_series_nonneg {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : TriadicCoeffFamily d) (_hq : 0 ≤ q) (hsq : 0 ≤ s * q) : 0 ≤ ∑' (n : ℕ), geometricWeight s q n * (maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)

theorem HCPolySupport.Book.Ch02.LambdaSqFinite_rpow_q_div_two_eq_tsum {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : TriadicCoeffFamily d) (hq : 0 < q) (hsq : 0 ≤ s * q) : (LambdaSq Q s (MultiscaleExponent.finite q) a).rpow (q / 2) = ∑' (n : ℕ), geometricWeight s q n * (maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)

theorem HCPolySupport.Book.Ch02.lambdaSqFinite_rpow_neg_q_div_two_eq_tsum {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : TriadicCoeffFamily d) (hq : 0 < q) (hsq : 0 ≤ s * q) : (lambdaSq Q s (MultiscaleExponent.finite q) a).rpow (-q / 2) = ∑' (n : ℕ), geometricWeight s q n * (maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)