Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.HomogenizationError

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

q = 1 homogenization-error theorems

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 ≤ s) (hR : R ∈ descendantsAtScale Q k) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : 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.homogenizationErrorOnCube_infinity_one_descendantsAtScale_le {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 ≤ s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : (finsetSsup (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.homogenizationErrorOnCube_infinity_one_basic_properties_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {t s lam Lam : ℝ} (hs : 0 < s) (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ∧ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ HomogenizationErrorOnCube Q t MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ∧ ∀ {k : ℤ}, k ≤ Q.scale → (finsetSsup (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.oneCubeDefect_rpow_half_sSup_le_homogenizationErrorOnCube_infinity_one_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : (sSup {m : ℝ | ∃ (e : FullBlockVec d), fullBlockVecNormSq e = 1 ∧ have P := ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixInvSqrt a0) e); have Q' := ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixSqrt a0) e); m = 1 / 2 * ResponseJ (cubeSet Q) (P.1 - Q'.2) (Q'.1 - P.2) a + 1 / 2 * ResponseJ (cubeSet Q) (Q'.2 + P.1) (Q'.1 + P.2) (adjointCoeffField a)}).rpow (1 / 2) ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_note_basic_properties_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {t s lam Lam : ℝ} (hs : 0 < s) (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : (sSup {m : ℝ | ∃ (e : FullBlockVec d), fullBlockVecNormSq e = 1 ∧ have P := ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixInvSqrt a0) e); have Q' := ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixSqrt a0) e); m = 1 / 2 * ResponseJ (cubeSet Q) (P.1 - Q'.2) (Q'.1 - P.2) a + 1 / 2 * ResponseJ (cubeSet Q) (Q'.2 + P.1) (Q'.1 + P.2) (adjointCoeffField a)}).rpow (1 / 2) ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ∧ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ HomogenizationErrorOnCube Q t MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ∧ ∀ {k : ℤ}, k ≤ Q.scale → (finsetSsup (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