Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Foundation.Basic

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

Foundational lemmas for multiscale deterministic quantities

This file collects the shared helper lemmas and the first structural wrappers used by the later MultiscaleQuantitiesBasic submodules.

def HCPolySupport.OpenCubeDeterministicCoarseData {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : Prop

Existence of deterministic coarse response matrices on the open cube, with the canonical block matrix representation and invertible σ*.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.OpenCubeDescendantDeterministicCoarseData {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : Prop

Deterministic coarse response data on every descendant open cube at scales no greater than Q.scale.

Equations

• HCPolySupport.OpenCubeDescendantDeterministicCoarseData Q a = ∀ l ≤ Q.scale, ∀ R ∈ HCPolySupport.descendantsAtScale Q l, HCPolySupport.OpenCubeDeterministicCoarseData R a

theorem HCPolySupport.OpenCubeDescendantDeterministicCoarseData.self {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDescendantDeterministicCoarseData Q a) : OpenCubeDeterministicCoarseData Q a

theorem HCPolySupport.responseJ_formula_coarseBlockMatrix_openCubeSet_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) (p q : Vec d) : ResponseJ (openCubeSet Q) p q a = 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (openCubeSet Q) a).lowerRight q) - vecDot p q - vecDot q (matVecMul (coarseBlockMatrix (openCubeSet Q) a).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (openCubeSet Q) a).upperLeft p)

Standalone quadratic formula for ResponseJ on a triadic open cube, packaged from the canonical deterministic coarse-data witness. This is the theorem surface intended for downstream deterministic and probabilistic chapters that should not need to unpack the individual coarse witnesses by hand.

theorem HCPolySupport.responseJ_formula_canonical_openCubeSet_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) (p q : Vec d) : ResponseJ (openCubeSet Q) p q a = 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse (openCubeSet Q) a) q) - vecDot p q + vecDot q (matVecMul (sigmaStarInvCoarse (openCubeSet Q) a) (matVecMul (kappaCoarse (openCubeSet Q) a) p)) + 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)) p)

Canonical coarse-variable version of the standalone quadratic ResponseJ formula on a triadic open cube. This is a note-facing reformulation of responseJ_formula_coarseBlockMatrix_openCubeSet_of_deterministicCoarseData.

theorem HCPolySupport.responseJ_zero_formula_coarseBlockMatrix_openCubeSet_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) (p : Vec d) : ResponseJ (openCubeSet Q) p 0 a = 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (openCubeSet Q) a).upperLeft p)

Coarse-block q = 0 quadratic formula for ResponseJ on a triadic open cube, with all deterministic coarse witnesses discharged by OpenCubeDeterministicCoarseData.

theorem HCPolySupport.responseJ_zero_formula_canonical_openCubeSet_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) (p : Vec d) : ResponseJ (openCubeSet Q) p 0 a = 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)) p)

Canonical q = 0 quadratic formula for ResponseJ on a triadic open cube, with all deterministic coarse witnesses discharged by OpenCubeDeterministicCoarseData.

theorem HCPolySupport.fullBlockVecNormSq_nonneg {d : ℕ} (x : FullBlockVec d) : 0 ≤ fullBlockVecNormSq x

theorem HCPolySupport.matNormSq_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matNormSq A

theorem HCPolySupport.matNorm_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matNorm A

theorem HCPolySupport.matNorm_eq_norm {d : ℕ} (A : Mat d) : matNorm A = ‖A‖

theorem HCPolySupport.norm_descendantsAverageMat_le_descendantsAverage_norm {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : ‖descendantsAverageMat Q j F‖ ≤ descendantsAverage Q j fun (R : TriadicCube d) => ‖F R‖

theorem HCPolySupport.matNorm_descendantsAverageMat_le_descendantsAverage_matNorm {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : matNorm (descendantsAverageMat Q j F) ≤ descendantsAverage Q j fun (R : TriadicCube d) => matNorm (F R)

@[simp]

theorem HCPolySupport.finsetAverage_singleton {α : Type u_1} (a : α) (f : α → ℝ) : finsetAverage {a} f = f a

@[simp]

theorem HCPolySupport.finsetSsup_singleton {α : Type u_1} (a : α) (f : α → ℝ) : finsetSsup {a} f = f a

theorem HCPolySupport.finsetAverage_le_finsetSsup {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (f : α → ℝ) : finsetAverage s f ≤ finsetSsup s f

theorem HCPolySupport.descendantsAverage_le_finsetSsup {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : TriadicCube d → ℝ) : descendantsAverage Q j f ≤ finsetSsup (descendantsAtDepth Q j) f

theorem HCPolySupport.matNorm_descendantsAverageMat_le_finsetSsup_matNorm {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : matNorm (descendantsAverageMat Q j F) ≤ finsetSsup (descendantsAtDepth Q j) fun (R : TriadicCube d) => matNorm (F R)

theorem HCPolySupport.sigmaStarInvCoarse_posSemidef_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : Matrix.PosSemidef (sigmaStarInvCoarse U a)

theorem HCPolySupport.bCoarse_posSemidef_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) : Matrix.PosSemidef (bCoarse sigma sigmaStar kappa)

theorem HCPolySupport.bCoarse_canonical_posSemidef_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.PosSemidef (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))

theorem HCPolySupport.coarseBlockMatrix_upperLeft_posSemidef_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.PosSemidef (coarseBlockMatrix U a).upperLeft

theorem HCPolySupport.coarseBlockMatrix_lowerRight_posSemidef_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.PosSemidef (coarseBlockMatrix U a).lowerRight

theorem HCPolySupport.sigmaStarInvCoarse_openCubeSet_posSemidef_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) : Matrix.PosSemidef (sigmaStarInvCoarse (openCubeSet Q) a)

Positive semidefiniteness of the canonical sigmaStarInvCoarse matrix on an open triadic cube, with the sigma-star coarse witness hidden inside OpenCubeDeterministicCoarseData.

theorem HCPolySupport.bCoarse_canonical_openCubeSet_posSemidef_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) : Matrix.PosSemidef (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a))

Positive semidefiniteness of the canonical bCoarse matrix on an open triadic cube, with the raw sigma/kappa/coarse witnesses hidden inside OpenCubeDeterministicCoarseData.

theorem HCPolySupport.coarseBlockMatrix_upperLeft_openCubeSet_posSemidef_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) : Matrix.PosSemidef (coarseBlockMatrix (openCubeSet Q) a).upperLeft

Positive semidefiniteness of the upper-left deterministic coarse block on an open triadic cube, with all raw deterministic coarse witnesses hidden inside OpenCubeDeterministicCoarseData.

theorem HCPolySupport.coarseBlockMatrix_lowerRight_openCubeSet_posSemidef_of_deterministicCoarseData {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} (hData : OpenCubeDeterministicCoarseData Q a) : Matrix.PosSemidef (coarseBlockMatrix (openCubeSet Q) a).lowerRight

Positive semidefiniteness of the lower-right deterministic coarse block on an open triadic cube, with all raw deterministic coarse witnesses hidden inside OpenCubeDeterministicCoarseData.

theorem HCPolySupport.coarseBlockMatrix_cubeSet_eq_openCubeSet_of_triadicCube {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) : coarseBlockMatrix (cubeSet Q) a = coarseBlockMatrix (openCubeSet Q) a

theorem HCPolySupport.descendantsAverageMat_posSemidef {d : ℕ} {Q : TriadicCube d} {j : ℕ} {F : TriadicCube d → Mat d} (hF : ∀ R ∈ descendantsAtDepth Q j, Matrix.PosSemidef (F R)) : Matrix.PosSemidef (descendantsAverageMat Q j F)

theorem HCPolySupport.matNormSq_eq_trace_transpose_mul {d : ℕ} (A : Mat d) : matNormSq A = (Matrix.transpose A * A).trace

theorem HCPolySupport.matNormSq_eq_trace_mul_transpose {d : ℕ} (A : Mat d) : matNormSq A = (A * Matrix.transpose A).trace

theorem HCPolySupport.matNormSq_eq_trace_mul_self_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) : matNormSq A = (A * A).trace

theorem HCPolySupport.matNormSq_eq_trace_pow_two_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) : matNormSq A = (A ^ 2).trace

theorem HCPolySupport.matLoewnerLE_sub_posSemidef_of_posSemidef {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : Matrix.PosSemidef (B - A)

theorem HCPolySupport.matNormSq_le_of_matLoewnerLE_of_posSemidef {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : matNormSq A ≤ matNormSq B

theorem HCPolySupport.matNorm_le_of_matLoewnerLE_of_posSemidef {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : matNorm A ≤ matNorm B

@[simp]

theorem HCPolySupport.geometricDiscount_one_eq (s : ℝ) : geometricDiscount s 1 = 1 - Real.rpow 3 (-s)

@[simp]

theorem HCPolySupport.geometricWeight_one_eq (s : ℝ) (n : ℕ) : geometricWeight s 1 n = geometricDiscount s 1 * Real.rpow 3 (-s * ↑n)