Coarse-graining support:

Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.OriginCube

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

MuOrdering -- origin-cube specializations

Origin-cube openCubeSet and cubeSet specializations of the sigmaStarCoarse_le_sigmaCoarse, sigmaCoarse_le_bCoarse, and kappaCoarse_add_transpose ≤ sigmaCoarse - sigmaStarCoarse orderings.

theorem HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_openCubeSet_originCube_of_isEllipticFieldOn {d : ℕ} {n : ℤ} (a : CoeffField d) {lam Lam : ℝ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) (p : Vec d) : vecDot p (matVecMul (sigmaStarCoarse (openCubeSet (originCube d n)) a) p) ≤ vecDot p (matVecMul (sigmaCoarse (openCubeSet (originCube d n)) a) p)

theorem HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_cubeSet_originCube_of_isEllipticFieldOn {d : ℕ} [NeZero d] {n : ℤ} (a : CoeffField d) {lam Lam : ℝ} (R : PotentialSolenoidalL2RecoveryData (cubeSet (originCube d n))) (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (cubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (cubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa) (p : Vec d) : vecDot p (matVecMul (sigmaStarCoarse (cubeSet (originCube d n)) a) p) ≤ vecDot p (matVecMul (sigmaCoarse (cubeSet (originCube d n)) a) p)

theorem HCPolySupport.sigmaCoarse_le_bCoarse_openCubeSet_originCube_of_isEllipticFieldOn {d : ℕ} {n : ℤ} (a : CoeffField d) {lam Lam : ℝ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) : MatLoewnerLE (sigmaCoarse (openCubeSet (originCube d n)) a) (bCoarse (sigmaCoarse (openCubeSet (originCube d n)) a) (sigmaStarCoarse (openCubeSet (originCube d n)) a) (kappaCoarse (openCubeSet (originCube d n)) a))

theorem HCPolySupport.sigmaCoarse_le_bCoarse_cubeSet_originCube_of_isEllipticFieldOn {d : ℕ} [NeZero d] {n : ℤ} (a : CoeffField d) {lam Lam : ℝ} (R : PotentialSolenoidalL2RecoveryData (cubeSet (originCube d n))) (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa) : MatLoewnerLE (sigmaCoarse (cubeSet (originCube d n)) a) (bCoarse (sigmaCoarse (cubeSet (originCube d n)) a) (sigmaStarCoarse (cubeSet (originCube d n)) a) (kappaCoarse (cubeSet (originCube d n)) a))

theorem HCPolySupport.kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse_cube {d : ℕ} {n : ℤ} (a : CoeffField d) {lam Lam : ℝ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) (p : Vec d) : vecDot p (matVecMul (kappaCoarse (openCubeSet (originCube d n)) a + matTranspose (kappaCoarse (openCubeSet (originCube d n)) a)) p) ≤ vecDot p (matVecMul (sigmaCoarse (openCubeSet (originCube d n)) a - sigmaStarCoarse (openCubeSet (originCube d n)) a) p)

theorem HCPolySupport.kappaCoarse_add_transpose_le_sigmaDifference_originCube_elliptic {d : ℕ} [NeZero d] {n : ℤ} (a : CoeffField d) {lam Lam : ℝ} (R : PotentialSolenoidalL2RecoveryData (cubeSet (originCube d n))) (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (cubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (cubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa) (p : Vec d) : vecDot p (matVecMul (kappaCoarse (cubeSet (originCube d n)) a + matTranspose (kappaCoarse (cubeSet (originCube d n)) a)) p) ≤ vecDot p (matVecMul (sigmaCoarse (cubeSet (originCube d n)) a - sigmaStarCoarse (cubeSet (originCube d n)) a) p)