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

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

Basic Helpers 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.

@[simp]

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_eq {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : TriadicCoeffFamily d) (a0 : Mat d) : scaleResponseAtScale Q k MultiscaleExponent.infinity a a0 = (maxDescendantNormalizedBlockResponseAtScale Q k a a0).rpow (1 / 2)

@[simp]

theorem HCPolySupport.Book.Ch02.homogenizationErrorFinite_infinity_one_eq_tsum {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (a : TriadicCoeffFamily d) (a0 : Mat d) : HomogenizationErrorFinite Q n s MultiscaleExponent.infinity 1 a a0 = ∑' (l : ℕ), geometricWeight s 1 l * scaleResponseAtScale Q (n - ↑l) MultiscaleExponent.infinity a a0

@[simp]

theorem HCPolySupport.Book.Ch02.homogenizationErrorOnCube_infinity_one_eq_tsum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : TriadicCoeffFamily d) (a0 : Mat d) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 = ∑' (l : ℕ), geometricWeight s 1 l * scaleResponseAtScale Q (Q.scale - ↑l) MultiscaleExponent.infinity a a0

@[simp]

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_self {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : maxDescendantNormalizedBlockResponseAtScale Q Q.scale a a0 = normalizedBlockResponseMax Q a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_self_eq {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 = (normalizedBlockResponseMax Q a a0).rpow (1 / 2)

theorem HCPolySupport.Book.Ch02.finsetAverageReal_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (φ : α → β) (hφ : Set.InjOn φ ↑s) (f : β → ℝ) (g : α → ℝ) (hfg : ∀ x ∈ s, f (φ x) = g x) : finsetAverageReal (Finset.image φ s) f = finsetAverageReal s g

Average over a finite image, specialized to the public Chapter 2 finsetAverageReal convention.

theorem HCPolySupport.Book.Ch02.translateCube_injective {d : ℕ} (z : Fin d → ℤ) : Function.Injective (translateCube z)

Translating triadic cube indices by a fixed shift is injective.