Coarse-graining support: #
Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.SigmaStarLeSigma
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
MuOrdering -- sigmaStarCoarse ≤ sigmaCoarse bridges #
The three elliptic-bridge wrappers establishing sigmaStarCoarse U a ≤ sigmaCoarse U a from IsEllipticFieldOn plus a domain regularity hypothesis
(HodgeConverseCriterion, IsOpenBoundedConvexDomain, or
IsSobolevRegularDomain).
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_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)
(p : Vec d)
:
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_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)
(p : Vec d)
:
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_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))
(p : Vec d)
: