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

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

Response and scale-response infrastructure

theorem HCPolySupport.normalizedBlockResponseMax_le_maxDescendantNormalizedBlockResponseAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) : normalizedBlockResponseMax R a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.normalizedBlockResponseValueSet_nonempty {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) : (normalizedBlockResponseValueSet Q a a0).Nonempty

theorem HCPolySupport.normalizedBlockResponseValueSet_bddAbove_of_isEllipticFieldOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : BddAbove (normalizedBlockResponseValueSet Q a a0)

theorem HCPolySupport.ResponseJ_cubeSet_eq_openCubeSet_of_triadicCube_reproved {d : ℕ} [NeZero d] (Q : TriadicCube d) (p q : Vec d) (a : CoeffField d) : ResponseJ (cubeSet Q) p q a = ResponseJ (openCubeSet Q) p q a

theorem HCPolySupport.normalizedBlockResponseValueSet_eq_half_responseJ_adjoint_sum_set_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))] (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : normalizedBlockResponseValueSet Q a a0 = {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)}

theorem HCPolySupport.normalizedBlockResponseMax_eq_sSup_half_responseJ_adjoint_sum_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))] (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : normalizedBlockResponseMax Q 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)}

theorem HCPolySupport.scaleResponse_self_eq_sqrt_responseJ_adjoint_sum {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))] (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : scaleResponseAtScale Q Q.scale 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)

theorem HCPolySupport.normalizedBlockResponseMax_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) : 0 ≤ normalizedBlockResponseMax Q a a0

theorem HCPolySupport.maxDescendantNormalizedBlockResponseAtScale_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k l : ℤ} (a : CoeffField d) (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantNormalizedBlockResponseAtScale R l a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q l a a0

theorem HCPolySupport.normalizedBlockResponseMax_le_maxDescendantNormalizedBlockResponseAtScale_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : normalizedBlockResponseMax Q a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.maxDescendantNormalizedBlockResponseAtScale_le_of_le_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) {k l : ℤ} (hkl : k ≤ l) (hlQ : l ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : maxDescendantNormalizedBlockResponseAtScale Q l a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.maxDescendantBBlockNormAtScale_le_of_le_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) {k l : ℤ} (hkl : k ≤ l) (hlQ : l ≤ Q.scale) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : maxDescendantBBlockNormAtScale Q l a ≤ maxDescendantBBlockNormAtScale Q k a

theorem HCPolySupport.maxDescendantSigmaStarInvNormAtScale_le_of_le_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) {k l : ℤ} (hkl : k ≤ l) (hlQ : l ≤ Q.scale) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : maxDescendantSigmaStarInvNormAtScale Q l a ≤ maxDescendantSigmaStarInvNormAtScale Q k a

theorem HCPolySupport.maxDescendantBBlockNormAtScale_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) : 0 ≤ maxDescendantBBlockNormAtScale Q k a

theorem HCPolySupport.maxDescendantSigmaStarInvNormAtScale_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) : 0 ≤ maxDescendantSigmaStarInvNormAtScale Q k a

theorem HCPolySupport.maxDescendantNormalizedBlockResponseAtScale_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) : 0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.scaleResponseAtScale_infinity_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) : 0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0

theorem HCPolySupport.scaleResponseAtScale_infinity_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k l : ℤ} (a : CoeffField d) (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : scaleResponseAtScale R l MultiscaleExponent.infinity a a0 ≤ scaleResponseAtScale Q l MultiscaleExponent.infinity a a0

theorem HCPolySupport.scaleResponseAtScale_infinity_le_of_le_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) {k l : ℤ} (hkl : k ≤ l) (hlQ : l ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : scaleResponseAtScale Q l MultiscaleExponent.infinity a a0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0

theorem HCPolySupport.scaleResponseAtScale_infinity_self_le_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0

theorem HCPolySupport.scaleResponse_infinity_self_le_homogenizationError {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 : Summable fun (n : ℕ) => geometricWeight s 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

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_le_of_lt_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {t s lam Lam : ℝ} (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ HomogenizationErrorOnCube Q t MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0