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

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

The p = infinity, q = 1 HCPolySupport Error Route

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

theorem HCPolySupport.Book.Ch02.summable_homogenizationErrorOnCube_infinity_one_terms {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch02.HomogenizationErrorOnCube_infinity_one_nonneg {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) : 0 ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_self_le_homogenizationErrorOnCube_infinity_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) : scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch02.homogenizationErrorOnCube_infinity_one_le_of_lt {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) {t s : ℝ} (ht : 0 < t) (hts : t < s) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ HomogenizationErrorOnCube Q t MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch02.homogenizationErrorOnCube_infinity_one_le_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) (hR : R ∈ descendantsAtScale Q k) : HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch02.homogenizationErrorOnCube_infinity_one_descendantsAtScale_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) : (finsetSupReal (descendantsAtScale Q k) fun (R : TriadicCube d) => HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0) ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch02.homogenizationErrorInfinityOneBasicTheory {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : HomogenizationErrorInfinityOneBasicTheory Q a a0

Public proof package for the p = infinity, q = 1 basic properties of the homogenization error.