Documentation

Mathlib.LinearAlgebra.Matrix.HadamardMatrix

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 #

source
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 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.

Instances For
    source
    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
    source
    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
    source
    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.

    source
    @[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
    source
    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.

    source
    @[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
    source
    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.

    source
    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: only a constant sum hypothesis on one side is needed under the two-sided orthogonality condition.

    source
    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.

    source
    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.

    source
    @[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
    source
    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.

    source
    @[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.

    source
    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).

    source
    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).

    source
    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.

    source
    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.

    source
    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.

    source
    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
    source
    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.