Coarse-graining support: Support.CoarseGraining.AdjointSymmetry.BasicAdjoint

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

Adjoint symmetry -- basic adjoint-coefficient-field equalities

blockVecFlipFlux / blockMatFlipFlux, muValueSet_adjointCoeffField_flipFlux, Mu_adjointCoeffField_flipFlux, and the coarseBlockMatrix / coarseStarredBlockMatrixInv adjointCoeffField equalities (including the component variants for upperLeft / upperRight / lowerLeft / lowerRight).

def HCPolySupport.blockVecFlipFlux {d : ℕ} (P : BlockVec d) : BlockVec d

Flip the flux component of a doubled block vector.

Equations

• HCPolySupport.blockVecFlipFlux P = (P.1, -P.2)

def HCPolySupport.blockMatFlipFlux {d : ℕ} (A : BlockMat d) : BlockMat d

Flip the off-diagonal flux signs of a doubled block matrix.

Equations

• HCPolySupport.blockMatFlipFlux A = { upperLeft := A.upperLeft, upperRight := -A.upperRight, lowerLeft := -A.lowerLeft, lowerRight := A.lowerRight }

@[simp]

theorem HCPolySupport.blockVecFlipFlux_flipFlux {d : ℕ} (P : BlockVec d) : blockVecFlipFlux (blockVecFlipFlux P) = P

@[simp]

theorem HCPolySupport.blockState_flipFlux_flipFlux {d : ℕ} (X : BlockState d) : X.flipFlux.flipFlux = X

@[simp]

theorem HCPolySupport.adjointCoeffField_adjointCoeffField {d : ℕ} (a : CoeffField d) : adjointCoeffField (adjointCoeffField a) = a

@[simp]

theorem HCPolySupport.blockMatVecMul_blockMatFlipFlux {d : ℕ} (A : BlockMat d) (P : BlockVec d) : blockMatVecMul (blockMatFlipFlux A) P = blockVecFlipFlux (blockMatVecMul A (blockVecFlipFlux P))

theorem HCPolySupport.blockVecDot_blockVecFlipFlux_right {d : ℕ} (P Q : BlockVec d) : blockVecDot P (blockVecFlipFlux Q) = blockVecDot (blockVecFlipFlux P) Q

@[simp]

theorem HCPolySupport.blockReflect_blockMatFlipFlux {d : ℕ} (A : BlockMat d) : blockReflect (blockMatFlipFlux A) = blockMatFlipFlux (blockReflect A)

theorem HCPolySupport.isBlockMuAdmissible_flipFlux {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : IsBlockMuAdmissible U (blockVecFlipFlux P) X.flipFlux

theorem HCPolySupport.blockEnergyDensity_adjointCoeffField_flipFlux {d : ℕ} (a : CoeffField d) (X : BlockState d) (x : Vec d) : blockEnergyDensity (adjointCoeffField a) X.flipFlux x = blockEnergyDensity a X x

theorem HCPolySupport.volumeAverage_blockEnergyDensity_adjointCoeffField_flipFlux {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X : BlockState d) : volumeAverage U (blockEnergyDensity (adjointCoeffField a) X.flipFlux) = volumeAverage U (blockEnergyDensity a X)

theorem HCPolySupport.muValueSet_adjointCoeffField_flipFlux {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : muValueSet U (blockVecFlipFlux P) (adjointCoeffField a) = muValueSet U P a

theorem HCPolySupport.Mu_adjointCoeffField_flipFlux {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : Mu U (blockVecFlipFlux P) (adjointCoeffField a) = Mu U P a

def HCPolySupport.fullBlockVecFlipFluxLinearMap {d : ℕ} : FullBlockVec d →ₗ[ℝ] FullBlockVec d

The full-coordinate linear map flipping the flux half of a block vector.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.fullBlockVecFlipFluxLinearMap_toFullBlockVec {d : ℕ} (P : BlockVec d) : fullBlockVecFlipFluxLinearMap (toFullBlockVec P) = toFullBlockVec (blockVecFlipFlux P)

theorem HCPolySupport.hasQuadraticMu_adjointCoeffField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hquad : HasQuadraticMu U a) : HasQuadraticMu U (adjointCoeffField a)

theorem HCPolySupport.IsCoarseBlockMatrix.adjointCoeffField_symm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {Abar : BlockMat d} (hA : IsCoarseBlockMatrix U a Abar) : IsCoarseBlockMatrix U (adjointCoeffField a) (blockMatFlipFlux Abar)

theorem HCPolySupport.coarseBlockMatrix_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : coarseBlockMatrix U (adjointCoeffField a) = blockMatFlipFlux (coarseBlockMatrix U a)

theorem HCPolySupport.coarseBlockMatrix_lowerLeft_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseBlockMatrix U (adjointCoeffField a)).lowerLeft = -(coarseBlockMatrix U a).lowerLeft

theorem HCPolySupport.coarseBlockMatrix_upperLeft_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseBlockMatrix U (adjointCoeffField a)).upperLeft = (coarseBlockMatrix U a).upperLeft

theorem HCPolySupport.coarseBlockMatrix_upperRight_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseBlockMatrix U (adjointCoeffField a)).upperRight = -(coarseBlockMatrix U a).upperRight

theorem HCPolySupport.coarseBlockMatrix_lowerRight_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseBlockMatrix U (adjointCoeffField a)).lowerRight = (coarseBlockMatrix U a).lowerRight

theorem HCPolySupport.coarseStarredBlockMatrixInv_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : coarseStarredBlockMatrixInv U (adjointCoeffField a) = blockMatFlipFlux (coarseStarredBlockMatrixInv U a)

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).upperLeft = (coarseStarredBlockMatrixInv U a).upperLeft

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperRight_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).upperRight = -(coarseStarredBlockMatrixInv U a).upperRight

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerLeft_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).lowerLeft = -(coarseStarredBlockMatrixInv U a).lowerLeft

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_adjointCoeffField_of_exists {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).lowerRight = (coarseStarredBlockMatrixInv U a).lowerRight

theorem HCPolySupport.coarseBlockMatrix_adjointCoeffField_eq_blockMatFlipFlux_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : coarseBlockMatrix U (adjointCoeffField a) = blockMatFlipFlux (coarseBlockMatrix U a)

Generic-domain note-facing transpose compatibility for the canonical coarse block matrix \mathbf A(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseBlockMatrix_upperLeft_adjointCoeffField_eq_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseBlockMatrix U (adjointCoeffField a)).upperLeft = (coarseBlockMatrix U a).upperLeft

Generic-domain note-facing transpose compatibility for the upper-left block of \mathbf A(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseBlockMatrix_upperRight_adjointCoeffField_of_exists_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseBlockMatrix U (adjointCoeffField a)).upperRight = -(coarseBlockMatrix U a).upperRight

Generic-domain note-facing transpose compatibility for the upper-right block of \mathbf A(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseBlockMatrix_lowerLeft_adjointCoeffField_of_exists_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseBlockMatrix U (adjointCoeffField a)).lowerLeft = -(coarseBlockMatrix U a).lowerLeft

Generic-domain note-facing transpose compatibility for the lower-left block of \mathbf A(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseBlockMatrix_lowerRight_adjointCoeffField_eq_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseBlockMatrix U (adjointCoeffField a)).lowerRight = (coarseBlockMatrix U a).lowerRight

Generic-domain note-facing transpose compatibility for the lower-right block of \mathbf A(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseStarredBlockMatrixInv_adjointCoeffField_of_exists_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : coarseStarredBlockMatrixInv U (adjointCoeffField a) = blockMatFlipFlux (coarseStarredBlockMatrixInv U a)

Generic-domain note-facing transpose compatibility for the canonical starred inverse block matrix \mathbf A_*^{-1}(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_adjointCoeffField_eq_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).upperLeft = (coarseStarredBlockMatrixInv U a).upperLeft

Generic-domain note-facing transpose compatibility for the upper-left block of \mathbf A_*^{-1}(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperRight_adjointCoeffField_of_exists_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).upperRight = -(coarseStarredBlockMatrixInv U a).upperRight

Generic-domain note-facing transpose compatibility for the upper-right block of \mathbf A_*^{-1}(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerLeft_adjointCoeffField_of_exists_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).lowerLeft = -(coarseStarredBlockMatrixInv U a).lowerLeft

Generic-domain note-facing transpose compatibility for the lower-left block of \mathbf A_*^{-1}(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_adjointCoeffField_eq_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) : (coarseStarredBlockMatrixInv U (adjointCoeffField a)).lowerRight = (coarseStarredBlockMatrixInv U a).lowerRight

Generic-domain note-facing transpose compatibility for the lower-right block of \mathbf A_*^{-1}(U; a) packaged from recovery data and ellipticity.

theorem HCPolySupport.sigmaStarInvCoarse_adjointCoeffField_eq_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) : sigmaStarInvCoarse U (adjointCoeffField a) = sigmaStarInvCoarse U a

theorem HCPolySupport.sigmaStarInvCoarse_adjointCoeffField_eq_of_isSigmaStarData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) : sigmaStarInvCoarse U (adjointCoeffField a) = sigmaStarInvCoarse U a

Note-facing transpose compatibility for \sigma_*^{-1}(U; a) from primal and adjoint \sigma_* witness data.

theorem HCPolySupport.sigmaStarCoarse_adjointCoeffField_eq_of_isSigmaStarCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) : sigmaStarCoarse U (adjointCoeffField a) = sigmaStarCoarse U a

theorem HCPolySupport.coarseBlockMatrix_lowerLeft_eq_zero_of_adjointCoeffField_eq_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (hAdj : adjointCoeffField a = a) : (coarseBlockMatrix U a).lowerLeft = 0

If the coefficient field is self-adjoint, then the lower-left block of the canonical coarse block matrix vanishes.

theorem HCPolySupport.coarseBlockMatrix_upperRight_eq_zero_of_adjointCoeffField_eq_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (R : PotentialSolenoidalL2RecoveryData U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (compat : R.MuRecoveryCompatibilityData (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol)) (hAdj : adjointCoeffField a = a) : (coarseBlockMatrix U a).upperRight = 0

If the coefficient field is self-adjoint, then the upper-right block of the canonical coarse block matrix vanishes.