Coarse-graining support: #
Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.SigmaCoarsePosDef
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
MuOrdering -- sigmaCoarse positive-definiteness bridges #
The three elliptic-bridge wrappers establishing (sigmaCoarse U a).PosDef from
IsEllipticFieldOn plus a domain regularity hypothesis
(IsSobolevRegularDomain, HodgeConverseCriterion, or
IsOpenBoundedConvexDomain).
theorem
HCPolySupport.sigmaCoarse_posDef_of_isEllipticFieldOn_of_isSobolevRegularDomain
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : IsSobolevRegularDomain U)
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
{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.PosDef (sigmaCoarse U a)
theorem
HCPolySupport.sigmaCoarse_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))
{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)
:
Matrix.PosDef (sigmaCoarse U a)
theorem
HCPolySupport.sigmaCoarse_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))
{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)
:
Matrix.PosDef (sigmaCoarse U a)