Coarse-graining support: Support.CoarseGraining.MagicIdentities.BlockSubadditivity

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

Block-matrix and response-side subadditivity packages.

theorem HCPolySupport.magic_identity_responseJ_block_quadratic_coarseBlockMatrix_of_slice_formulas {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) (hRespUpper : ∀ (p : Vec d), ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix U a).upperLeft p)) (hRespMixed : ∀ (p q : Vec d), ResponseJ U p q a - ResponseJ U p 0 a - ResponseJ U 0 q a + vecDot p q = -vecDot q (matVecMul (coarseBlockMatrix U a).lowerLeft p)) (hRespLower : ∀ (q : Vec d), ResponseJ U 0 q a = 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix U a).lowerRight q)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix U a) (-p, q)) - vecDot p q

theorem HCPolySupport.magic_identity_responseJ_block_quadratic_coarseBlockMatrix_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)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix U a) (-p, q)) - vecDot p q

theorem HCPolySupport.coarseBlockMatrix_subadditive_openCubeSet_descendantsAtDepth_pair_of_isSigmaCoarse {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet Q) a (deterministicCoarseBlockMatrix (openCubeSet Q) a)) (hSQ : IsSigmaStarCoarse (openCubeSet Q) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet Q) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet Q) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (p q : Vec d) : 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q))

theorem HCPolySupport.coarseBlockMatrix_subadditive_blockQuadratic_on_openDescendants {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet Q) a (deterministicCoarseBlockMatrix (openCubeSet Q) a)) (hSQ : IsSigmaStarCoarse (openCubeSet Q) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet Q) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet Q) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) X) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) X)

theorem HCPolySupport.coarseBlockMatrix_upperLeft_subadditive_openCubeSet_descendantsAtDepth_of_isSigmaCoarse {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet Q) a (deterministicCoarseBlockMatrix (openCubeSet Q) a)) (hSQ : IsSigmaStarCoarse (openCubeSet Q) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet Q) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet Q) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (p : Vec d) : 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (openCubeSet Q) a).upperLeft p) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (openCubeSet R) a).upperLeft p)

theorem HCPolySupport.coarseBlockMatrix_lowerRight_subadditive_openCubeSet_descendantsAtDepth_of_isSigmaCoarse {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet Q) a (deterministicCoarseBlockMatrix (openCubeSet Q) a)) (hSQ : IsSigmaStarCoarse (openCubeSet Q) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet Q) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet Q) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (q : Vec d) : 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (openCubeSet Q) a).lowerRight q) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (openCubeSet R) a).lowerRight q)

theorem HCPolySupport.coarseBlockMatrix_subadditive_pair_on_originDescendants {d : ℕ} (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (p q : Vec d) : 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet (originCube d n)) a) (-p, q)) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q))

theorem HCPolySupport.coarseMatrix_subadditive_cube_descendants_blockQuadratic_of_isSigmaCoarse {d : ℕ} (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (openCubeSet (originCube d n)) a) X) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) X)

theorem HCPolySupport.coarseBlockMatrix_subadditive_openCubeSet_descendantsAtDepth_in_loewner_order_of_isSigmaCoarse {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet Q) a (deterministicCoarseBlockMatrix (openCubeSet Q) a)) (hSQ : IsSigmaStarCoarse (openCubeSet Q) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet Q) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet Q) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) : BlockMatLoewnerLE (coarseBlockMatrix (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (openCubeSet R) a)

theorem HCPolySupport.coarseMatrix_subadditive_cube_descendants_in_loewner_order {d : ℕ} [NeZero d] (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) : BlockMatLoewnerLE (coarseBlockMatrix (cubeSet (originCube d n)) a) (descendantsAverageBlockMat (originCube d n) j fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a)

theorem HCPolySupport.coarseBlockMatrix_upperLeft_subadditive_openCubeSet_originCube_descendantsAtDepth_of_isSigmaCoarse {d : ℕ} (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (p : Vec d) : 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (openCubeSet (originCube d n)) a).upperLeft p) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (openCubeSet R) a).upperLeft p)

theorem HCPolySupport.coarseBlockLowerRight_subadditive_on_originDescendants {d : ℕ} (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (q : Vec d) : 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (openCubeSet (originCube d n)) a).lowerRight q) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (openCubeSet R) a).lowerRight q)

theorem HCPolySupport.coarseBlockMatrix_subadditive_cubeSet_originCube_descendantsAtDepth_pair_of_isSigmaCoarse {d : ℕ} [NeZero d] (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (p q : Vec d) : 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a) (-p, q)) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (cubeSet R) a) (-p, q))

theorem HCPolySupport.coarseBlockMatrix_subadditive_blockQuadratic_on_cubeDescendants {d : ℕ} [NeZero d] (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a) X) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (cubeSet R) a) X)

theorem HCPolySupport.coarseBlockMatrix_upperLeft_subadditive_cubeSet_originCube_descendantsAtDepth_of_isSigmaCoarse {d : ℕ} [NeZero d] (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (p : Vec d) : 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a).upperLeft p) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix (cubeSet R) a).upperLeft p)

theorem HCPolySupport.coarseBlockMatrix_lowerRight_subadditive_cubeSet_originCube_descendantsAtDepth_of_isSigmaCoarse {d : ℕ} [NeZero d] (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (hAQ : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hSQ : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStarQ) (hKQ : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStarQ kappaQ) (hSigmaQ : IsSigmaCoarse (openCubeSet (originCube d n)) a sigmaQ sigmaStarQ kappaQ) (hdetQ : IsUnit (Matrix.det sigmaStarQ)) (hDesc : ∀ R ∈ descendantsAtDepth (originCube d n) j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (q : Vec d) : 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a).lowerRight q) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix (cubeSet R) a).lowerRight q)

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

theorem HCPolySupport.ResponseJ_cubeSet_eq_openCubeSet_of_triadicCube {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.isSigmaStarCoarse_cubeSet_iff_openCubeSet_of_triadicCube {d : ℕ} [NeZero d] (Q : TriadicCube d) {a : CoeffField d} {sigmaStar : Mat d} : IsSigmaStarCoarse (cubeSet Q) a sigmaStar ↔ IsSigmaStarCoarse (openCubeSet Q) a sigmaStar

theorem HCPolySupport.isKappaCoarse_cubeSet_iff_openCubeSet_of_triadicCube {d : ℕ} [NeZero d] (Q : TriadicCube d) {a : CoeffField d} {sigmaStar kappa : Mat d} : IsKappaCoarse (cubeSet Q) a sigmaStar kappa ↔ IsKappaCoarse (openCubeSet Q) a sigmaStar kappa

theorem HCPolySupport.isSigmaCoarse_cubeSet_iff_openCubeSet_of_triadicCube {d : ℕ} [NeZero d] (Q : TriadicCube d) {a : CoeffField d} {sigma sigmaStar kappa : Mat d} : IsSigmaCoarse (cubeSet Q) a sigma sigmaStar kappa ↔ IsSigmaCoarse (openCubeSet Q) a sigma sigmaStar kappa

theorem HCPolySupport.sigmaStarInvCoarse_cubeSet_eq_openCubeSet {d : ℕ} [NeZero d] (Q : TriadicCube d) {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse (openCubeSet Q) a sigmaStar) : sigmaStarInvCoarse (cubeSet Q) a = sigmaStarInvCoarse (openCubeSet Q) a

theorem HCPolySupport.bCoarse_sigmaCoarse_sigmaStarCoarse_kappaCoarse_cube_eq_cube {d : ℕ} [NeZero d] (Q : TriadicCube d) {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse (openCubeSet Q) a sigmaStar) (hK : IsKappaCoarse (openCubeSet Q) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet Q) a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : bCoarse (sigmaCoarse (cubeSet Q) a) (sigmaStarCoarse (cubeSet Q) a) (kappaCoarse (cubeSet Q) a) = bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)