Coarse-graining support: Support.Book.Ch05.Theorems.Section57.HomogenizationErrorClosed

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

Closed finite-q homogenization-error bounds

This file packages the deterministic summation step in the form used by the Section 5.7 minimal-scale corollary: once every scale response is controlled by one algebraic envelope, the whole finite-q multiscale error is controlled by the same envelope.

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorFinite_le_of_scaleResponseEnvelope {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A R : ℝ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hR : 0 ≤ R) (hscale : ∀ (l : ℕ), Ch02.scaleResponseAtScale Q (n - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * R) : Ch02.HomogenizationError Q n r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) a a0 ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹ * A.rpow q * R.rpow q).rpow (1 / q)

Closed finite-q \mathcal E control from one scale-by-scale envelope.

The displayed right-hand side is the geometric summation constant times the q-power of the single envelope. In applications R is the collapsed minimal-scale factor, for instance sqrt ((3^m / X)^(-alpha)).

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorFinite_le_const_mul_of_scaleResponseEnvelope {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A R : ℝ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hR : 0 ≤ R) (hscale : ∀ (l : ℕ), Ch02.scaleResponseAtScale Q (n - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * R) : have Cgeom := (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹).rpow (1 / q); Ch02.HomogenizationError Q n r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) a a0 ≤ Cgeom * A * R

Same as homogenizationErrorFinite_le_of_scaleResponseEnvelope, with the geometric constant pulled out of the q-root.

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnCube_le_of_scaleResponseEnvelope {d : ℕ} (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A R : ℝ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hR : 0 ≤ R) (hscale : ∀ (l : ℕ), Ch02.scaleResponseAtScale Q (Q.scale - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * R) : Ch02.HomogenizationErrorOnCube Q r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) a a0 ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹ * A.rpow q * R.rpow q).rpow (1 / q)

Closed finite-q control on a whole cube.

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnCube_le_const_mul_of_scaleResponseEnvelope {d : ℕ} (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A R : ℝ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hR : 0 ≤ R) (hscale : ∀ (l : ℕ), Ch02.scaleResponseAtScale Q (Q.scale - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * R) : have Cgeom := (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹).rpow (1 / q); Ch02.HomogenizationErrorOnCube Q r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) a a0 ≤ Cgeom * A * R

Whole-cube version with the geometric constant pulled out.

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnOriginCube_le_of_scaleResponseMinimalEnvelope {d m : ℕ} (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A X alpha : ℝ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hX : 0 < X) (hscale : ∀ (l : ℕ), Ch02.scaleResponseAtScale (originCube d ↑m) (↑m - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * √((3 ^ m / X) ^ (-alpha))) : Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) a a0 ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X) ^ (-alpha))

Origin-cube version with the minimal-scale factor already collapsed into X. This is the deterministic target shape for the Section 5.7 stochastic corollary.