Coarse-graining support: Support.CoarseGraining.OriginCubeSymmetry

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

noncomputable def HCPolySupport.BlockState.signFlip {d : ℕ} (X : BlockState d) (i : Fin d) : BlockState d

Coordinate sign-flip transport of a doubled state field.

Equations

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

noncomputable def HCPolySupport.BlockState.swap {d : ℕ} (X : BlockState d) (i j : Fin d) : BlockState d

Coordinate swap transport of a doubled state field.

Equations

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

@[simp]

theorem HCPolySupport.BlockState.signFlip_signFlip {d : ℕ} (X : BlockState d) (i : Fin d) : (X.signFlip i).signFlip i = X

@[simp]

theorem HCPolySupport.BlockState.swap_swap {d : ℕ} (X : BlockState d) (i j : Fin d) : (X.swap i j).swap i j = X

@[simp]

theorem HCPolySupport.blockVecConj_signFlipMatrix_signFlipMatrix {d : ℕ} (P : BlockVec d) (i : Fin d) : blockVecConj (signFlipMatrix i) (blockVecConj (signFlipMatrix i) P) = P

@[simp]

theorem HCPolySupport.blockVecConj_swap_swap {d : ℕ} (P : BlockVec d) (i j : Fin d) : blockVecConj (Matrix.swap ℝ i j) (blockVecConj (Matrix.swap ℝ i j) P) = P

@[simp]

theorem HCPolySupport.rotateCoeffField_signFlipMatrix_signFlipMatrix {d : ℕ} (a : CoeffField d) (i : Fin d) : rotateCoeffField (signFlipMatrix i) (rotateCoeffField (signFlipMatrix i) a) = a

@[simp]

theorem HCPolySupport.rotateCoeffField_swap_swap {d : ℕ} (a : CoeffField d) (i j : Fin d) : rotateCoeffField (Matrix.swap ℝ i j) (rotateCoeffField (Matrix.swap ℝ i j) a) = a

theorem HCPolySupport.isBlockMuAdmissible_signFlip_openCubeSet_originCube {d : ℕ} {n : ℤ} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible (openCubeSet (originCube d n)) P X) (i : Fin d) : IsBlockMuAdmissible (openCubeSet (originCube d n)) (blockVecConj (signFlipMatrix i) P) (X.signFlip i)

theorem HCPolySupport.isBlockMuAdmissible_swap_openCubeSet_originCube {d : ℕ} {n : ℤ} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible (openCubeSet (originCube d n)) P X) (i j : Fin d) : IsBlockMuAdmissible (openCubeSet (originCube d n)) (blockVecConj (Matrix.swap ℝ i j) P) (X.swap i j)

theorem HCPolySupport.blockEnergyDensity_rotateCoeffField_signFlip {d : ℕ} (a : CoeffField d) (X : BlockState d) (i : Fin d) (x : Vec d) : blockEnergyDensity (rotateCoeffField (signFlipMatrix i) a) (X.signFlip i) x = blockEnergyDensity a X ((signFlipVecContinuousLinearEquiv i) x)

theorem HCPolySupport.blockEnergyDensity_rotateCoeffField_swap {d : ℕ} (a : CoeffField d) (X : BlockState d) (i j : Fin d) (x : Vec d) : blockEnergyDensity (rotateCoeffField (Matrix.swap ℝ i j) a) (X.swap i j) x = blockEnergyDensity a X ((swapVecContinuousLinearEquiv i j) x)

theorem HCPolySupport.volumeAverage_blockEnergyDensity_signFlip_openCubeSet_originCube {d : ℕ} (n : ℤ) (a : CoeffField d) (X : BlockState d) (i : Fin d) : volumeAverage (openCubeSet (originCube d n)) (blockEnergyDensity (rotateCoeffField (signFlipMatrix i) a) (X.signFlip i)) = volumeAverage (openCubeSet (originCube d n)) (blockEnergyDensity a X)

theorem HCPolySupport.volumeAverage_blockEnergyDensity_swap_openCubeSet_originCube {d : ℕ} (n : ℤ) (a : CoeffField d) (X : BlockState d) (i j : Fin d) : volumeAverage (openCubeSet (originCube d n)) (blockEnergyDensity (rotateCoeffField (Matrix.swap ℝ i j) a) (X.swap i j)) = volumeAverage (openCubeSet (originCube d n)) (blockEnergyDensity a X)

theorem HCPolySupport.muValueSet_signFlip_openCubeSet_originCube {d : ℕ} (n : ℤ) (P : BlockVec d) (a : CoeffField d) (i : Fin d) : muValueSet (openCubeSet (originCube d n)) (blockVecConj (signFlipMatrix i) P) (rotateCoeffField (signFlipMatrix i) a) = muValueSet (openCubeSet (originCube d n)) P a

theorem HCPolySupport.muValueSet_swap_openCubeSet_originCube {d : ℕ} (n : ℤ) (P : BlockVec d) (a : CoeffField d) (i j : Fin d) : muValueSet (openCubeSet (originCube d n)) (blockVecConj (Matrix.swap ℝ i j) P) (rotateCoeffField (Matrix.swap ℝ i j) a) = muValueSet (openCubeSet (originCube d n)) P a

theorem HCPolySupport.Mu_signFlip_openCubeSet_originCube {d : ℕ} (n : ℤ) (P : BlockVec d) (a : CoeffField d) (i : Fin d) : Mu (openCubeSet (originCube d n)) (blockVecConj (signFlipMatrix i) P) (rotateCoeffField (signFlipMatrix i) a) = Mu (openCubeSet (originCube d n)) P a

theorem HCPolySupport.Mu_swap_openCubeSet_originCube {d : ℕ} (n : ℤ) (P : BlockVec d) (a : CoeffField d) (i j : Fin d) : Mu (openCubeSet (originCube d n)) (blockVecConj (Matrix.swap ℝ i j) P) (rotateCoeffField (Matrix.swap ℝ i j) a) = Mu (openCubeSet (originCube d n)) P a

theorem HCPolySupport.IsCoarseBlockMatrix.signFlip_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} {Abar : BlockMat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i : Fin d) : IsCoarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (signFlipMatrix i) a) (blockMatConj (signFlipMatrix i) Abar)

theorem HCPolySupport.IsCoarseBlockMatrix.swap_openCubeSet_originCube {d : ℕ} {n : ℤ} {a : CoeffField d} {Abar : BlockMat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i j : Fin d) : IsCoarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (Matrix.swap ℝ i j) a) (blockMatConj (Matrix.swap ℝ i j) Abar)

theorem HCPolySupport.coarseBlockMatrix_signFlip_openCubeSet_originCube_of_exists {d : ℕ} {n : ℤ} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i : Fin d) : coarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (signFlipMatrix i) a) = blockMatConj (signFlipMatrix i) (coarseBlockMatrix (openCubeSet (originCube d n)) a)

theorem HCPolySupport.coarseBlockMatrix_swap_openCubeSet_originCube_of_exists {d : ℕ} {n : ℤ} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i j : Fin d) : coarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (Matrix.swap ℝ i j) a) = blockMatConj (Matrix.swap ℝ i j) (coarseBlockMatrix (openCubeSet (originCube d n)) a)

theorem HCPolySupport.coarseBlockMatrix_upperLeft_signFlip_openCubeSet_originCube_of_exists {d : ℕ} {n : ℤ} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i : Fin d) : (coarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (signFlipMatrix i) a)).upperLeft = signFlipMatrix i * (coarseBlockMatrix (openCubeSet (originCube d n)) a).upperLeft * signFlipMatrix i

theorem HCPolySupport.coarseBlockMatrix_lowerRight_signFlip_openCubeSet_originCube_of_exists {d : ℕ} {n : ℤ} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i : Fin d) : (coarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (signFlipMatrix i) a)).lowerRight = signFlipMatrix i * (coarseBlockMatrix (openCubeSet (originCube d n)) a).lowerRight * signFlipMatrix i

theorem HCPolySupport.coarseBlockMatrix_upperLeft_swap_openCubeSet_originCube_of_exists {d : ℕ} {n : ℤ} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i j : Fin d) : (coarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (Matrix.swap ℝ i j) a)).upperLeft = Matrix.swap ℝ i j * (coarseBlockMatrix (openCubeSet (originCube d n)) a).upperLeft * Matrix.swap ℝ i j

theorem HCPolySupport.coarseBlockMatrix_lowerRight_swap_openCubeSet_originCube_of_exists {d : ℕ} {n : ℤ} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar) (i j : Fin d) : (coarseBlockMatrix (openCubeSet (originCube d n)) (rotateCoeffField (Matrix.swap ℝ i j) a)).lowerRight = Matrix.swap ℝ i j * (coarseBlockMatrix (openCubeSet (originCube d n)) a).lowerRight * Matrix.swap ℝ i j