Coarse-graining support: Support.Probability.Scalarization

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

noncomputable def HCPolySupport.signFlipMatrix {d : ℕ} (i : Fin d) : Mat d

The diagonal sign-flip matrix that changes the sign of the i-th coordinate.

Equations

• HCPolySupport.signFlipMatrix i = Matrix.diagonal fun (j : Fin d) => if j = i then -1 else 1

def HCPolySupport.IsSignFlipInvariant {d : ℕ} (A : Mat d) : Prop

Invariance under conjugation by every coordinate sign flip.

Equations

• HCPolySupport.IsSignFlipInvariant A = ∀ (i : Fin d), HCPolySupport.signFlipMatrix i * A * HCPolySupport.signFlipMatrix i = A

def HCPolySupport.IsSwapInvariant {d : ℕ} (A : Mat d) : Prop

Invariance under conjugation by every coordinate transposition matrix.

Equations

• HCPolySupport.IsSwapInvariant A = ∀ (i j : Fin d), Matrix.swap ℝ i j * A * Matrix.swap ℝ i j = A

def HCPolySupport.IsScalarMatrix {d : ℕ} (A : Mat d) : Prop

Scalar matrices over Fin d, written as multiples of the identity.

Equations

• HCPolySupport.IsScalarMatrix A = ∃ (c : ℝ), A = c • 1

theorem HCPolySupport.signFlipMatrix_mul_mul_signFlipMatrix_apply {d : ℕ} (i r c : Fin d) (A : Mat d) : (signFlipMatrix i * A * signFlipMatrix i) r c = (if r = i then -1 else 1) * A r c * if c = i then -1 else 1

theorem HCPolySupport.signFlipMatrix_sq {d : ℕ} (i : Fin d) : signFlipMatrix i * signFlipMatrix i = 1

theorem HCPolySupport.offDiag_eq_zero_of_isSignFlipInvariant {d : ℕ} {A : Mat d} (hA : IsSignFlipInvariant A) {i j : Fin d} (hij : i ≠ j) : A i j = 0

theorem HCPolySupport.diag_eq_of_isSwapInvariant {d : ℕ} {A : Mat d} (hA : IsSwapInvariant A) (i j : Fin d) : A i i = A j j

theorem HCPolySupport.isScalarMatrix_of_isSignFlipInvariant_of_isSwapInvariant {d : ℕ} [NeZero d] {A : Mat d} (hFlip : IsSignFlipInvariant A) (hSwap : IsSwapInvariant A) : IsScalarMatrix A

theorem HCPolySupport.isSignFlipInvariant_of_isScalarMatrix {d : ℕ} {A : Mat d} (hA : IsScalarMatrix A) : IsSignFlipInvariant A

theorem HCPolySupport.isSwapInvariant_of_isScalarMatrix {d : ℕ} {A : Mat d} (hA : IsScalarMatrix A) : IsSwapInvariant A

theorem HCPolySupport.isScalarMatrix_inv {d : ℕ} {A : Mat d} (hA : IsScalarMatrix A) : IsScalarMatrix A⁻¹

theorem HCPolySupport.skewPart_eq_zero_of_isScalarMatrix {d : ℕ} {A : Mat d} (hA : IsScalarMatrix A) : skewPart A = 0