Coarse-graining support: Support.Geometry.SignedPermutation

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

def HCPolySupport.intVecToRealVec {d : ℕ} (z : Fin d → ℤ) : Vec d

The real-vector representation of an integer lattice vector.

Equations

• HCPolySupport.intVecToRealVec z i = ↑(z i)

def HCPolySupport.IsSignedPermutationMatrix {d : ℕ} (R : Mat d) : Prop

A coordinate permutation with independent sign changes.

Equations

• HCPolySupport.IsSignedPermutationMatrix R = ∃ (σ : Equiv.Perm (Fin d)) (s : Fin d → ℝ), (∀ (i : Fin d), s i = 1 ∨ s i = -1) ∧ ∀ (i j : Fin d), R i j = if i = σ j then s j else 0

theorem HCPolySupport.matVecMul_one_signedPermutation {d : ℕ} (x : Vec d) : matVecMul 1 x = x

theorem HCPolySupport.IsSignedPermutationMatrix.transpose_mul_self {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) : matTranspose R * R = 1

theorem HCPolySupport.IsSignedPermutationMatrix.mul_transpose_self {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) : R * matTranspose R = 1

theorem HCPolySupport.IsSignedPermutationMatrix.transpose {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) : IsSignedPermutationMatrix (matTranspose R)

theorem HCPolySupport.IsSignedPermutationMatrix.det_ne_zero {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) : Matrix.det R ≠ 0

theorem HCPolySupport.IsSignedPermutationMatrix.abs_det_eq_one {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) : |Matrix.det R| = 1

theorem HCPolySupport.continuous_matVecMul_signedPermutation {d : ℕ} (R : Mat d) : Continuous fun (x : Vec d) => matVecMul R x

noncomputable def HCPolySupport.signedPermutationHomeomorph {d : ℕ} (R : Mat d) (hR : IsSignedPermutationMatrix R) : Vec d ≃ₜ Vec d

The homeomorphism x ↦ R x for a signed permutation matrix, with inverse x ↦ Rᵀ x.

Equations

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

theorem HCPolySupport.measurePreserving_matVecMul_signedPermutation {d : ℕ} {R : Mat d} (hR : IsSignedPermutationMatrix R) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => matVecMul R x) MeasureTheory.volume MeasureTheory.volume