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

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

Translation Covariance for Chapter 2.5 HCPolySupport Error

This file proves the public basic properties of the homogenization error \mathcal E_{s,\infty,1} from Sec. 2.5.

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_translateCube_of_normalizedBlockResponseMax {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (a0 : Mat d) {k : ℤ} (hk : k ≤ Q.scale) (hJ : ∀ R ∈ descendantsAtScale Q k, normalizedBlockResponseMax (translateCube (descendantTranslationShift (Q.scale - k).toNat z) R) a a0 = normalizedBlockResponseMax R b a0) : maxDescendantNormalizedBlockResponseAtScale (translateCube z Q) k a a0 = maxDescendantNormalizedBlockResponseAtScale Q k b a0

Translation covariance of descendant normalized-response maxima, reduced to one-cube normalized-response covariance.

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_translateCube_of_normalizedBlockResponseMax {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (a0 : Mat d) {k : ℤ} (hk : k ≤ Q.scale) (p : MultiscaleExponent) (hJ : ∀ R ∈ descendantsAtScale Q k, normalizedBlockResponseMax (translateCube (descendantTranslationShift (Q.scale - k).toNat z) R) a a0 = normalizedBlockResponseMax R b a0) : scaleResponseAtScale (translateCube z Q) k p a a0 = scaleResponseAtScale Q k p b a0

Translation covariance of the scale-level response aggregation, reduced to one-cube normalized-response covariance.

theorem HCPolySupport.Book.Ch02.HomogenizationErrorFinite_translateCube_of_normalizedBlockResponseMax {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (s : ℝ) (p : MultiscaleExponent) (q : ℝ) (a0 : Mat d) (hJ : ∀ (l : ℕ), ∀ R ∈ descendantsAtScale Q (n - ↑l), normalizedBlockResponseMax (translateCube (descendantTranslationShift (Q.scale - (n - ↑l)).toNat z) R) a a0 = normalizedBlockResponseMax R b a0) : HomogenizationErrorFinite (translateCube z Q) n s p q a a0 = HomogenizationErrorFinite Q n s p q b a0

Translation covariance of finite-q homogenization error, reduced to one-cube normalized-response covariance on all descendant scales used by the series.

theorem HCPolySupport.Book.Ch02.HomogenizationErrorInfinity_translateCube_of_normalizedBlockResponseMax {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (s : ℝ) (p : MultiscaleExponent) (a0 : Mat d) (hJ : ∀ (l : ℕ), ∀ R ∈ descendantsAtScale Q (n - ↑l), normalizedBlockResponseMax (translateCube (descendantTranslationShift (Q.scale - (n - ↑l)).toNat z) R) a a0 = normalizedBlockResponseMax R b a0) : HomogenizationErrorInfinity (translateCube z Q) n s p a a0 = HomogenizationErrorInfinity Q n s p b a0

Translation covariance of endpoint homogenization error, reduced to one-cube normalized-response covariance on all descendant scales used by the supremum.

theorem HCPolySupport.Book.Ch02.HomogenizationError_translateCube_of_normalizedBlockResponseMax {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d) (hJ : ∀ (l : ℕ), ∀ R ∈ descendantsAtScale Q (n - ↑l), normalizedBlockResponseMax (translateCube (descendantTranslationShift (Q.scale - (n - ↑l)).toNat z) R) a a0 = normalizedBlockResponseMax R b a0) : HomogenizationError (translateCube z Q) n s p q a a0 = HomogenizationError Q n s p q b a0

Translation covariance of homogenization error, reduced to one-cube normalized-response covariance.

theorem HCPolySupport.Book.Ch02.HomogenizationErrorOnCube_translateCube_of_normalizedBlockResponseMax {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d) (hJ : ∀ (l : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑l), normalizedBlockResponseMax (translateCube (descendantTranslationShift l z) R) a a0 = normalizedBlockResponseMax R b a0) : HomogenizationErrorOnCube (translateCube z Q) s p q a a0 = HomogenizationErrorOnCube Q s p q b a0

Translation covariance of the on-cube homogenization error, reduced to one-cube normalized-response covariance.