Coarse-graining support:

Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.SigmaStarPosDef

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

MuOrdering -- sigmaStar / sigmaStarInv positive-definiteness wrappers

Positive-definiteness lemmas for sigmaStarInvCoarse and sigmaStarCoarse under IsSigmaStarCoarse, the elliptic field plus HodgeConverseCriterion / IsOpenBoundedConvexDomain bridges, and the corresponding IsUnit / determinant wrappers.

theorem HCPolySupport.sigmaStarInvCoarse_posDef_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hU : IsSobolevRegularDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : Matrix.PosDef (sigmaStarInvCoarse U a)

theorem HCPolySupport.isUnit_det_sigmaStarInvCoarse_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hU : IsSobolevRegularDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : IsUnit (Matrix.det (sigmaStarInvCoarse U a))

theorem HCPolySupport.isUnit_det_of_isSigmaStarCoarse_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hU : IsSobolevRegularDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : IsUnit (Matrix.det sigmaStar)

theorem HCPolySupport.sigmaStarInvCoarse_posDef_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : Matrix.PosDef (sigmaStarInvCoarse U a)

theorem HCPolySupport.isUnit_det_of_isSigmaStarCoarse_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : IsUnit (Matrix.det sigmaStar)

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

theorem HCPolySupport.sigmaStarInvCoarse_posDef_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.PosDef (sigmaStarInvCoarse U a)

theorem HCPolySupport.sigmaStarCoarse_posDef_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) : Matrix.PosDef (sigmaStarCoarse U a)

theorem HCPolySupport.sigmaStarCoarse_posDef_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hU : IsSobolevRegularDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hHodge : HodgeConverseCriterion U) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : Matrix.PosDef (sigmaStarCoarse U a)

theorem HCPolySupport.sigmaStarCoarse_posDef_of_isEllipticFieldOn_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) (hConv : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) : Matrix.PosDef (sigmaStarCoarse U a)