Coarse-graining support: #
Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.SigmaLeBCoarse
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
MuOrdering -- sigma ≤ bCoarse and Loewner orderings #
kappaTranspose_sigmaStarInvCoarse_kappa_posSemidef, the abstract
sigma_le_bCoarse_of_isSigmaStarCoarse Loewner ordering, and the canonical
sigmaCoarse ≤ bCoarse bridges via IsSigmaCoarse, IsEllipticFieldOn plus
HodgeConverseCriterion, and IsOpenBoundedConvexDomain.
theorem
HCPolySupport.kappaTranspose_sigmaStarInvCoarse_kappa_posSemidef
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
:
(matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a * kappaCoarse U a).PosSemidef
theorem
HCPolySupport.sigma_le_bCoarse_of_isSigmaStarCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
:
MatLoewnerLE sigma (bCoarse sigma sigmaStar kappa)
theorem
HCPolySupport.sigmaCoarse_le_bCoarse_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
:
MatLoewnerLE (sigmaCoarse U a) (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))
theorem
HCPolySupport.sigmaCoarse_le_bCoarse_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}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
:
MatLoewnerLE (sigmaCoarse U a) (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))
theorem
HCPolySupport.sigmaCoarse_le_bCoarse_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}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
:
MatLoewnerLE (sigmaCoarse U a) (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))