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

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

Starred-block and b-matrix subadditivity consequences.

theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cubeDescendants_blockQuadratic {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 (coarseStarredBlockMatrixInv (openCubeSet Q) a) X) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a) X)

theorem HCPolySupport.starredBlockInvUpperLeft_subadditive_on_openCubeDescendants {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 (coarseStarredBlockMatrixInv (openCubeSet Q) a).upperLeft p) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a).upperLeft p)

theorem HCPolySupport.starredBlockInvLowerRight_subadditive_on_openCubeDescendants {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 (coarseStarredBlockMatrixInv (openCubeSet Q) a).lowerRight q) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a).lowerRight q)

theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cube_descendants_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 (coarseStarredBlockMatrixInv (openCubeSet (originCube d n)) a) X) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a) X)

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_subadditive_cube_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 (coarseStarredBlockMatrixInv (openCubeSet (originCube d n)) a).upperLeft p) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a).upperLeft p)

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_subadditive_cube_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)) (q : Vec d) : 1 / 2 * vecDot q (matVecMul (coarseStarredBlockMatrixInv (openCubeSet (originCube d n)) a).lowerRight q) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a).lowerRight q)

theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cube_descendants_blockQuadratic {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 (coarseStarredBlockMatrixInv (cubeSet (originCube d n)) a) X) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseStarredBlockMatrixInv (cubeSet R) a) X)

theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cubeDescendants_in_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 (coarseStarredBlockMatrixInv (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseStarredBlockMatrixInv (openCubeSet R) a)

theorem HCPolySupport.coarseStarredBlockMatrixInv_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 (coarseStarredBlockMatrixInv (cubeSet (originCube d n)) a) (descendantsAverageBlockMat (originCube d n) j fun (R : TriadicCube d) => coarseStarredBlockMatrixInv (cubeSet R) a)

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_subadditive_cube_descendants {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 (coarseStarredBlockMatrixInv (cubeSet (originCube d n)) a).upperLeft p) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseStarredBlockMatrixInv (cubeSet R) a).upperLeft p)

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_subadditive_cube_descendants {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 (coarseStarredBlockMatrixInv (cubeSet (originCube d n)) a).lowerRight q) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseStarredBlockMatrixInv (cubeSet R) a).lowerRight q)

theorem HCPolySupport.sigmaStarInvCoarse_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} (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 (sigmaStarInvCoarse (openCubeSet Q) a) q) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse (openCubeSet R) a) q)

theorem HCPolySupport.sigmaStarInvCoarse_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} (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 (sigmaStarInvCoarse (openCubeSet (originCube d n)) a) q) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse (openCubeSet R) a) q)

theorem HCPolySupport.sigmaStarInvCoarse_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} (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 (sigmaStarInvCoarse (cubeSet (originCube d n)) a) q) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse (cubeSet R) a) q)

theorem HCPolySupport.sigmaStarInvCoarse_subadditive_descendants_in_loewnerOrder {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (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)) : MatLoewnerLE (sigmaStarInvCoarse (openCubeSet Q) a) (descendantsAverageMat Q j fun (R : TriadicCube d) => sigmaStarInvCoarse (openCubeSet R) a)

theorem HCPolySupport.sigmaStarInvCoarse_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} (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)) : MatLoewnerLE (sigmaStarInvCoarse (cubeSet (originCube d n)) a) (descendantsAverageMat (originCube d n) j fun (R : TriadicCube d) => sigmaStarInvCoarse (cubeSet R) a)

theorem HCPolySupport.bCoarse_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} (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 (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)) p) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse (openCubeSet R) a) (sigmaStarCoarse (openCubeSet R) a) (kappaCoarse (openCubeSet R) a)) p)

theorem HCPolySupport.bCoarse_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} (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 (bCoarse (sigmaCoarse (openCubeSet (originCube d n)) a) (sigmaStarCoarse (openCubeSet (originCube d n)) a) (kappaCoarse (openCubeSet (originCube d n)) a)) p) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse (openCubeSet R) a) (sigmaStarCoarse (openCubeSet R) a) (kappaCoarse (openCubeSet R) a)) p)

theorem HCPolySupport.bCoarse_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} (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 (bCoarse (sigmaCoarse (cubeSet (originCube d n)) a) (sigmaStarCoarse (cubeSet (originCube d n)) a) (kappaCoarse (cubeSet (originCube d n)) a)) p) ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse (cubeSet R) a) (sigmaStarCoarse (cubeSet R) a) (kappaCoarse (cubeSet R) a)) p)

theorem HCPolySupport.bCoarse_le_descendantAverage_in_loewnerOrder {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {sigmaQ sigmaStarQ kappaQ : Mat d} (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)) : MatLoewnerLE (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)) (descendantsAverageMat Q j fun (R : TriadicCube d) => bCoarse (sigmaCoarse (openCubeSet R) a) (sigmaStarCoarse (openCubeSet R) a) (kappaCoarse (openCubeSet R) a))

theorem HCPolySupport.bCoarse_subadditive_cubeSet_originCube_descendantsAtDepth_in_loewner_order_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} (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)) : MatLoewnerLE (bCoarse (sigmaCoarse (cubeSet (originCube d n)) a) (sigmaStarCoarse (cubeSet (originCube d n)) a) (kappaCoarse (cubeSet (originCube d n)) a)) (descendantsAverageMat (originCube d n) j fun (R : TriadicCube d) => bCoarse (sigmaCoarse (cubeSet R) a) (sigmaStarCoarse (cubeSet R) a) (kappaCoarse (cubeSet R) a))