Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticWrappers

Coarse-graining support: Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticWrappers #

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

MuOrdering -- elliptic no-hdet wrappers for core magic identities #

This file packages the most-used ResponseJ and block-quadratic magic identities, Mu - p · q formulas, and canonical ordering consequences under recovery-plus-ellipticity hypotheses, so downstream users do not need to thread IsUnit sigmaStar.det by hand.

source
theorem HCPolySupport.responseJ_zero_canonicalFormula_of_ellipticity_hodgeConverse {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) (p : Vec d) :
ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p)
source
theorem HCPolySupport.basic_cg_identities_responseJ_zero_formula_canonical_of_ellipticField {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) (p : Vec d) :
ResponseJ U p 0 a = 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p)
source
theorem HCPolySupport.basic_cg_identities_responseJ_formula_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} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (p q : Vec d) :
ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse U a) q) - vecDot p q + vecDot q (matVecMul (sigmaStarInvCoarse U a) (matVecMul (kappaCoarse U a) p)) + 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p)
source
theorem HCPolySupport.basic_cg_identities_responseJ_formula_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} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (p q : Vec d) :
ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse U a) q) - vecDot p q + vecDot q (matVecMul (sigmaStarInvCoarse U a) (matVecMul (kappaCoarse U a) p)) + 1 / 2 * vecDot p (matVecMul (bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a)) p)
source
theorem HCPolySupport.magic_identity_responseJ_completed_square_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} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (p q : Vec d) :
ResponseJ U p q a = sigmaCorrectedResponse U a p - vecDot p q + 1 / 2 * vecDot (q + matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_responseJ_completed_square_canonical_of_ellipticField {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) (p q : Vec d) :
ResponseJ U p q a = sigmaCorrectedResponse U a p - vecDot p q + 1 / 2 * vecDot (q + matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_responseJ_completed_square_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) (p q : Vec d) :
ResponseJ U p q a = 1 / 2 * vecDot p (matVecMul sigma p) - vecDot p q + 1 / 2 * vecDot (q + matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q + matVecMul kappa p))
source
theorem HCPolySupport.magic_identity_responseJ_completed_square_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) (p q : Vec d) :
ResponseJ U p q a = 1 / 2 * vecDot p (matVecMul sigma p) - vecDot p q + 1 / 2 * vecDot (q + matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q + matVecMul kappa p))
source
theorem HCPolySupport.basic_cg_identities_responseJ_formula_coarseMatrix_of_ellipticField {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 q : Vec d) :
ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix U a).lowerRight q) - vecDot p q - vecDot q (matVecMul (coarseBlockMatrix U a).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix U a).upperLeft p)
source
theorem HCPolySupport.basic_cg_identities_responseJ_formula_coarseMatrix_of_of_ellipticField {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 q : Vec d) :
ResponseJ U p q a = 1 / 2 * vecDot q (matVecMul (coarseBlockMatrix U a).lowerRight q) - vecDot p q - vecDot q (matVecMul (coarseBlockMatrix U a).lowerLeft p) + 1 / 2 * vecDot p (matVecMul (coarseBlockMatrix U a).upperLeft p)
source
theorem HCPolySupport.magic_identity_responseJ_block_quadratic_coarseMatrix_of_ellipticField {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 q : Vec d) :
ResponseJ U p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix U a) (-p, q)) - vecDot p q
source
theorem HCPolySupport.magic_identity_responseJ_block_quadratic_coarseMatrix_of_of_ellipticField {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 q : Vec d) :
ResponseJ U p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix U a) (-p, q)) - vecDot p q
source
theorem HCPolySupport.magic_identity_block_quadratic_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) (p q : Vec d) :
1 / 2 * blockVecDot (p, q) (blockMatVecMul (coarseBlockMatrix U a) (p, q)) = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_block_quadratic_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) (p q : Vec d) :
1 / 2 * blockVecDot (p, q) (blockMatVecMul (coarseBlockMatrix U a) (p, q)) = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_mu_sub_vecDot_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) (p q : Vec d) :
Mu U (p, q) a - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p)) - vecDot p q
source
theorem HCPolySupport.magic_identity_mu_sub_vecDot_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) (p q : Vec d) :
Mu U (p, q) a - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p)) - vecDot p q
source
theorem HCPolySupport.Mu_sub_pairing_shiftedSquare_canonical_of_ellipticity_hodge {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 q : Vec d) :
Mu U (p, q) a - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_mu_sub_vectorDot_shifted_square_of_ellipticField {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 q : Vec d) :
Mu U (p, q) a - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p))
source
theorem HCPolySupport.responseJ_add_Mu_sub_pairing_canonical_of_ellipticity_hodge {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 q h : Vec d) :
ResponseJ U p (q - h) a + (Mu U (p, q + h) a - vecDot p (q + h)) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + vecDot (q - matVecMul (sigmaStarCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a) p)) + vecDot (h - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (h - matVecMul (kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_responseJ_add_mu_sub_vectorDot_canonical {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 q h : Vec d) :
ResponseJ U p (q - h) a + (Mu U (p, q + h) a - vecDot p (q + h)) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + vecDot (q - matVecMul (sigmaStarCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a) p)) + vecDot (h - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (h - matVecMul (kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_responseJ_add_mu_sub_vectorDot_diagonal_canonical {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) :
ResponseJ U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a + (Mu U (p, matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) a - vecDot p (matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p)) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
source
theorem HCPolySupport.magic_identity_responseJ_add_mu_sub_vectorDot_diagonal_canonical_of_convexDomain {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) :
ResponseJ U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a + (Mu U (p, matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) a - vecDot p (matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p)) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
source
theorem HCPolySupport.magic_identity_mu_sub_vectorDot_sigmaStar_add_kappa_canonical {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) :
Mu U (p, matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) a - vecDot p (matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p)
source
theorem HCPolySupport.magic_identity_mu_sub_vectorDot_sigmaStar_add_kappa_canonical_of_kappa_canonical {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) :
Mu U (p, matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) a - vecDot p (matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p)
source
theorem HCPolySupport.kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse {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) :
vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) ≤ vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
source
theorem HCPolySupport.kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse_of_ellipticField {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) :
vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) ≤ vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
source
theorem HCPolySupport.kappa_add_transpose_le_sigma_sub_sigmaStar_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) :
vecDot p (matVecMul (kappa + matTranspose kappa) p) ≤ vecDot p (matVecMul (sigma - sigmaStar) p)
source
theorem HCPolySupport.kappa_add_transpose_le_sigma_sub_sigmaStar_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) :
vecDot p (matVecMul (kappa + matTranspose kappa) p) ≤ vecDot p (matVecMul (sigma - sigmaStar) p)
source
theorem HCPolySupport.sigmaStar_le_sigma_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) :
vecDot p (matVecMul sigmaStar p) ≤ vecDot p (matVecMul sigma p)
source
theorem HCPolySupport.sigmaStar_le_sigma_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) :
vecDot p (matVecMul sigmaStar p) ≤ vecDot p (matVecMul sigma p)
source
theorem HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vectorDot {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul sigma p) + 1 / 2 * vecDot (q - matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q - matVecMul kappa p)) - vecDot p q
source
theorem HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vectorDot_of_ellipticField {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul sigma p) + 1 / 2 * vecDot (q - matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q - matVecMul kappa p)) - vecDot p q
source
theorem HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_of_ellipticField {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) - 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStar + kappa) p) (matVecMul sigmaStar⁻¹ (q - matVecMul (sigmaStar + kappa) p))
source
theorem HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vectorDot_of_convexDomain {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) - 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStar + kappa) p) (matVecMul sigmaStar⁻¹ (q - matVecMul (sigmaStar + kappa) p))
source
theorem HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vectorDot_canonical {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p)) - vecDot p q
source
theorem HCPolySupport.magic_identity_mu_adjointField_flipFlux_sub_vectorDot_of_ellipticRecovery {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p)) - vecDot p q
source
theorem HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vectorDot_shifted_square {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p))
source
theorem HCPolySupport.magic_identity_mu_adjointField_flipFlux_shiftedSquare_of_ellipticRecovery {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 q : Vec d) :
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p))