Coarse-graining support:

Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.BCoarseCanonical

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

MuOrdering -- bCoarse canonical positive-definiteness and IsUnit

The three bCoarse_canonical_posDef_of_… wrappers (Sobolev-regular, HodgeConverseCriterion, IsOpenBoundedConvexDomain) and the matching isUnit_det_bCoarse_canonical_… wrappers obtained from the positive-definite plus determinant correspondence.

theorem HCPolySupport.bCoarse_canonical_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 (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))

theorem HCPolySupport.bCoarse_canonical_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 (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))

theorem HCPolySupport.bCoarse_canonical_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 (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a))

theorem HCPolySupport.isUnit_det_bCoarse_canonical_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)) : IsUnit (Matrix.det (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)))

theorem HCPolySupport.isUnit_det_bCoarse_canonical_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) : IsUnit (Matrix.det (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)))

theorem HCPolySupport.isUnit_det_bCoarse_canonical_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) : IsUnit (Matrix.det (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)))