Coarse-graining support: Support.Book.Ch02.Theorems.HomogenizationError.Finite

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

Finite exponent identities for the homogenization error

This file records the finite-q algebra for the public homogenization error. The first downstream use is the p = infinity, q = 2 route: after squaring, the square roots in the scale response disappear and \mathcal E is exactly the geometrically weighted sum of the normalized block-response maxima.

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_sq_eq {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : scaleResponseAtScale Q k MultiscaleExponent.infinity a a0 ^ 2 = maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_rpow_two_eq {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : (scaleResponseAtScale Q k MultiscaleExponent.infinity a a0).rpow 2 = maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch02.homogenizationErrorFinite_infinity_two_sq_eq_tsum {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) (a0 : Mat d) : HomogenizationErrorFinite Q n s MultiscaleExponent.infinity 2 a a0 ^ 2 = ∑' (l : ℕ), geometricWeight s 2 l * maxDescendantNormalizedBlockResponseAtScale Q (n - ↑l) a a0

theorem HCPolySupport.Book.Ch02.homogenizationErrorOnCube_infinity_two_sq_eq_tsum {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) (a0 : Mat d) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 2) a a0 ^ 2 = ∑' (l : ℕ), geometricWeight s 2 l * maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑l) a a0