Hadamard matrices

This file defines Matrix.IsHadamard, a unified notion that specializes to the classical real Hadamard matrices over ℝ/ℤ (where star is trivial and entries are ±1) and to the complex Hadamard matrices over ℂ (where entries have unit norm). Basic results: conjugate-transpose closure, the order identity n = s * star s from constant row or column sums, the Sylvester (Kronecker) construction, and the divisibility obstruction 4 ∣ n.

References

• [W. de Launey and D. L. Flannery, Algebraic Design Theory][deLauneyFlannery2011]

structure Matrix.IsHadamard {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] (A : Matrix n n R) : Prop

A square matrix over a *-semiring whose entries are unitary and whose rows and columns are orthogonal with respect to the conjugate transpose: A * Aᴴ = n • 1 and Aᴴ * A = n • 1.

Over a commutative ring in which the order is regular, the one-sided condition from [Definition 2.3.1][deLauneyFlannery2011] implies this predicate by IsHadamard.of_mul_conjTranspose; over a ring with trivial star (e.g. ℝ, ℤ), the entry condition becomes A i j = 1 ∨ A i j = -1. Over ℂ, the entry condition becomes ‖A i j‖ = 1, generalizing the fourth-root complex Hadamard matrices of [Definition 2.7.1][deLauneyFlannery2011].

• apply_mem (i j : n) : A i j ∈ unitary R
• mul_conjTranspose : A * A.conjTranspose = ↑(Fintype.card n) • 1
• conjTranspose_mul : A.conjTranspose * A = ↑(Fintype.card n) • 1

theorem Matrix.isHadamard_iff {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] (A : Matrix n n R) : A.IsHadamard ↔ (∀ (i j : n), A i j ∈ unitary R) ∧ A * A.conjTranspose = ↑(Fintype.card n) • 1 ∧ A.conjTranspose * A = ↑(Fintype.card n) • 1

theorem Matrix.IsHadamard.isStarNormal {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) : IsStarNormal A

theorem Matrix.IsHadamard.conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) : A.conjTranspose.IsHadamard

The conjugate transpose of a Hadamard matrix is Hadamard.

@[simp]

theorem Matrix.isHadamard_conjTranspose_iff {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} : A.conjTranspose.IsHadamard ↔ A.IsHadamard

theorem Matrix.IsHadamard.reindex {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} (e₁ e₂ : n ≃ m) (hA : A.IsHadamard) : ((Matrix.reindex e₁ e₂) A).IsHadamard

Permuting the rows and columns of a Hadamard matrix gives a Hadamard matrix.

@[simp]

theorem Matrix.isHadamard_submatrix_equiv_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} (e₁ e₂ : m ≃ n) : (A.submatrix ⇑e₁ ⇑e₂).IsHadamard ↔ A.IsHadamard

theorem Matrix.IsHadamard.kronecker {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix m m R} {B : Matrix n n R} (hA : A.IsHadamard) (hB : B.IsHadamard) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).IsHadamard

The Kronecker product of two Hadamard matrices is Hadamard.

theorem Matrix.IsHadamard.card_eq_mul_star_of_const_col_sum {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} {s : R} (hA : A.IsHadamard) (hcard : IsRegular ↑(Fintype.card n)) (hcol : ∀ (j : n), ∑ i : n, A i j = s) : ↑(Fintype.card n) = s * star s

A Hadamard matrix with constant column sum s has order s * star s, provided the order is regular in R.

The row-sum form is IsHadamard.card_eq_star_mul_of_const_row_sum; over a ring with trivial star the conclusion becomes (Fintype.card n : R) = s ^ 2, a slightly stronger form of [Theorem 2.3.7][deLauneyFlannery2011]: only a constant sum hypothesis on one side is needed under the two-sided orthogonality condition.

theorem Matrix.IsHadamard.card_eq_star_mul_of_const_row_sum {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [StarRing R] {A : Matrix n n R} {s : R} (hA : A.IsHadamard) (hcard : IsRegular ↑(Fintype.card n)) (hrow : ∀ (i : n), ∑ j : n, A i j = s) : ↑(Fintype.card n) = star s * s

A Hadamard matrix with constant row sum s has order star s * s, provided the order is regular in R. This generalizes [Theorem 2.3.7][deLauneyFlannery2011].

theorem Matrix.IsHadamard.transpose {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) : A.transpose.IsHadamard

The transpose of a Hadamard matrix is Hadamard.

Unlike IsHadamard.conjTranspose this requires commutativity: over a noncommutative ring the transpose of a Hadamard matrix need not be Hadamard.

@[simp]

theorem Matrix.isHadamard_transpose_iff {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] [StarRing R] {A : Matrix n n R} : A.transpose.IsHadamard ↔ A.IsHadamard

theorem Matrix.IsHadamard.neg {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Ring R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) : (-A).IsHadamard

Negating a Hadamard matrix gives a Hadamard matrix.

@[simp]

theorem Matrix.IsHadamard.neg_iff {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [Ring R] [StarRing R] {A : Matrix n n R} : (-A).IsHadamard ↔ A.IsHadamard

A matrix is Hadamard iff its negation is.

theorem Matrix.IsHadamard.det_mul_star_det {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n

The Hadamard determinant identity: det A * star (det A) = (card n)^(card n).

theorem Matrix.IsHadamard.star_det_mul_det {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) : star A.det * A.det = ↑(Fintype.card n) ^ Fintype.card n

The Hadamard determinant identity: star (det A) * det A = (card n)^(card n).

theorem Matrix.IsHadamard.det_ne_zero {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] {A : Matrix n n R} [IsReduced R] (hA : A.IsHadamard) (hcard : ↑(Fintype.card n) ≠ 0) : A.det ≠ 0

A Hadamard matrix over a reduced commutative ring has nonzero determinant, provided the order is nonzero in R.

theorem Matrix.IsHadamard.isRegular_det {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] {A : Matrix n n R} (hA : A.IsHadamard) (hcard : IsRegular ↑(Fintype.card n)) : IsRegular A.det

The determinant of a Hadamard matrix is regular, provided the order is regular in R.

theorem Matrix.IsHadamard.of_mul_conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] {A : Matrix n n R} (hentry : ∀ (i j : n), A i j ∈ unitary R) (hmul : A * A.conjTranspose = ↑(Fintype.card n) • 1) (hcard : IsRegular ↑(Fintype.card n)) : A.IsHadamard

Build a Hadamard matrix from the one-sided row-orthogonality condition, provided the order is regular in R.

This is the matrix form of [Theorem 2.3.6][deLauneyFlannery2011].

theorem Matrix.isHadamard_iff_mul_conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] {A : Matrix n n R} (hcard : IsRegular ↑(Fintype.card n)) : A.IsHadamard ↔ (∀ (i j : n), A i j ∈ unitary R) ∧ A * A.conjTranspose = ↑(Fintype.card n) • 1

theorem Matrix.IsHadamard.four_dvd_card {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsHadamard) (hcard : 2 < Fintype.card n) : 4 ∣ Fintype.card n

An integer Hadamard matrix of order greater than two has order divisible by four.

This is the standard divisibility obstruction in [Section 2.3][deLauneyFlannery2011].