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

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

A.E. Invariance 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.normalizedBlockResponseValueSet_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (a0 : Mat d) : normalizedBlockResponseValueSet Q a a0 = normalizedBlockResponseValueSet Q b a0

The normalized one-cube block-response value set depends only on the coefficient family modulo a.e. equality on each triadic cube.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseMax_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (a0 : Mat d) : normalizedBlockResponseMax Q a a0 = normalizedBlockResponseMax Q b a0

The normalized one-cube block-response maximum is a.e.-representative invariant.

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (k : ℤ) (a0 : Mat d) : maxDescendantNormalizedBlockResponseAtScale Q k a a0 = maxDescendantNormalizedBlockResponseAtScale Q k b a0

The descendant normalized block-response maximum is a.e.-representative invariant.

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (k : ℤ) (p : MultiscaleExponent) (a0 : Mat d) : scaleResponseAtScale Q k p a a0 = scaleResponseAtScale Q k p b a0

The scale-level response aggregation in the homogenization error is a.e.-representative invariant.

theorem HCPolySupport.Book.Ch02.HomogenizationErrorFinite_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (q : ℝ) (a0 : Mat d) : HomogenizationErrorFinite Q n s p q a a0 = HomogenizationErrorFinite Q n s p q b a0

The finite-q multiscale homogenization error is a.e.-representative invariant.

theorem HCPolySupport.Book.Ch02.HomogenizationErrorInfinity_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (a0 : Mat d) : HomogenizationErrorInfinity Q n s p a a0 = HomogenizationErrorInfinity Q n s p b a0

The endpoint-q multiscale homogenization error is a.e.-representative invariant.

theorem HCPolySupport.Book.Ch02.HomogenizationError_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d) : HomogenizationError Q n s p q a a0 = HomogenizationError Q n s p q b a0

The multiscale homogenization error is a.e.-representative invariant.

theorem HCPolySupport.Book.Ch02.HomogenizationErrorOnCube_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d) : HomogenizationErrorOnCube Q s p q a a0 = HomogenizationErrorOnCube Q s p q b a0

The untruncated cube homogenization error is a.e.-representative invariant.