Coarse-graining support: Support.CoarseGraining.MagicIdentities.MuOrdering.Identities #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
MuOrdering -- magic identities and sigmaStar <= sigma #
The magic-identity theorems (block_quadratic, mu_sub_vecDot, responseJ_add_mu_sub_vecDot and their shifted-square / canonical / deterministic variants), sigmaStarCoarse <= sigmaCoarse on origin cubes, and the kappa_add_transpose / sigmaStar <= sigma / sigmaStarCoarse <= sigmaCoarse general orderings under isSigmaCoarse + mu_ge_vecDot or IsEllipticFieldOn.
theorem
HCPolySupport.magic_identity_block_quadratic_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 q : Vec d)
:
theorem
HCPolySupport.magic_identity_block_quadratic_canonical_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 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))
theorem
HCPolySupport.magic_identity_block_quadratic_deterministicCoarseBlockMatrix_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 q : Vec d)
:
theorem
HCPolySupport.magic_identity_mu_sub_vecDot_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 q : Vec d)
:
theorem
HCPolySupport.magic_identity_mu_sub_vecDot_canonical_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 q : Vec d)
:
theorem
HCPolySupport.magic_identity_mu_sub_vecDot_shifted_square_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 q : Vec d)
:
theorem
HCPolySupport.magic_identity_mu_sub_vecDot_shifted_square_canonical_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 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))
theorem
HCPolySupport.magic_identity_responseJ_add_mu_sub_vecDot_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 q h : Vec d)
:
theorem
HCPolySupport.magic_identity_responseJ_add_mu_sub_vecDot_canonical_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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 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))
theorem
HCPolySupport.magic_identity_responseJ_add_mu_sub_vecDot_diagonal_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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)
:
theorem
HCPolySupport.magic_identity_responseJ_add_mu_sub_vecDot_diagonal_canonical_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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)
:
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)
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_openCubeSet_originCube_of_isSigmaCoarse
{d : ℕ}
{n : ℤ}
(a : CoeffField d)
{lam Lam : ℝ}
(R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n)))
(system : MuOperatorSystemData (openCubeSet (originCube d n)) a)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a)
(pairingIntegrable :
∀ (P Q : BlockVec d),
MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q))
(openCubeSet (originCube d n)) MeasureTheory.volume)
(mu_eq_muCandidate :
∀ (P : BlockVec d),
Mu (openCubeSet (originCube d n)) P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
{sigma sigmaStar kappa : Mat d}
(hA :
IsCoarseBlockMatrix (openCubeSet (originCube d n)) a
(deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a))
(hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar)
(hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa)
(hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
:
vecDot p (matVecMul (sigmaStarCoarse (openCubeSet (originCube d n)) a) p) ≤ vecDot p (matVecMul (sigmaCoarse (openCubeSet (originCube d n)) a) p)
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_cubeSet_originCube_of_isSigmaCoarse
{d : ℕ}
{n : ℤ}
(a : CoeffField d)
{lam Lam : ℝ}
(R : MuCorrectionSpaceRecoveryData (cubeSet (originCube d n)))
(system : MuOperatorSystemData (cubeSet (originCube d n)) a)
(hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a)
(pairingIntegrable :
∀ (P Q : BlockVec d),
MeasureTheory.IntegrableOn (blockPairingIntegrand a (R.recoveredField system P) (R.recoveredField system Q))
(cubeSet (originCube d n)) MeasureTheory.volume)
(mu_eq_muCandidate :
∀ (P : BlockVec d),
Mu (cubeSet (originCube d n)) P a = (system.toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
{sigma sigmaStar kappa : Mat d}
(hA : IsCoarseBlockMatrix (cubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (cubeSet (originCube d n)) a))
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
(hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa)
(hSigma : IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
:
vecDot p (matVecMul (sigmaStarCoarse (cubeSet (originCube d n)) a) p) ≤ vecDot p (matVecMul (sigmaCoarse (cubeSet (originCube d n)) a) p)
theorem
HCPolySupport.magic_identity_mu_sub_vecDot_sigmaStar_add_kappa_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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)
:
theorem
HCPolySupport.magic_identity_mu_sub_vecDot_sigmaStar_add_kappa_canonical_of_isSigmaCoarse
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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)
:
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)
theorem
HCPolySupport.kappa_add_transpose_le_sigma_sub_sigmaStar_of_isSigmaCoarse_of_mu_ge_vecDot
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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))
(hMuGe : ∀ (P : BlockVec d), vecDot P.1 P.2 ≤ Mu U P a)
(p : Vec d)
:
theorem
HCPolySupport.kappa_add_transpose_le_sigma_sub_sigmaStar_of_isEllipticFieldOn
{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)
(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)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
:
theorem
HCPolySupport.kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse_of_isSigmaCoarse_of_mu_ge_vecDot
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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))
(hMuGe : ∀ (P : BlockVec d), vecDot P.1 P.2 ≤ Mu U P a)
(p : Vec d)
:
vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) ≤ vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
theorem
HCPolySupport.kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse_of_isEllipticFieldOn
{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)
(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)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
:
vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) ≤ vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)
theorem
HCPolySupport.sigmaStar_le_sigma_of_isSigmaCoarse_of_mu_ge_vecDot
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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))
(hMuGe : ∀ (P : BlockVec d), vecDot P.1 P.2 ≤ Mu U P a)
(p : Vec d)
:
theorem
HCPolySupport.sigmaStar_le_sigma_of_isEllipticFieldOn
{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)
(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)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
:
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_of_isSigmaCoarse_of_mu_ge_vecDot
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
{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))
(hMuGe : ∀ (P : BlockVec d), vecDot P.1 P.2 ≤ Mu U P a)
(p : Vec d)
:
theorem
HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_of_isEllipticFieldOn
{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)
(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)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
: