Condition numbers of sign matrices

AbbreviationBoolean encoding of sign matrices#✓fully proved

For a natural number \(n\), a sign matrix of order \(n\) is encoded as an \(n \times n\) matrix with entries in the Booleans \(\{\mathrm{true}, \mathrm{false}\}\), whose rows and columns are indexed by \(\{0, \dots, n - 1\}\).

abbrev SignMatrix (n : ℕ) := Matrix (Fin n) (Fin n) Bool

Used by 8

Used byAdding the identity to a symmetric conference matrix gives a sign matrix · Boolean matrices realize exactly the sign matrices · Minimum condition number of sign matrices · The minimum condition number is attained · Minimum condition number of order one · The minimum condition number is at least one · Real sign matrix of a Boolean matrix · Realized sign matrices have entries \(\pm 1\)

DefinitionReal sign matrix of a Boolean matrix#✓fully proved

The realization of a Boolean \(n \times n\) matrix \(A\) is the real \(n \times n\) matrix whose \((i, j)\) entry is \(-1\) if \(A_{ij}\) is true and \(1\) if \(A_{ij}\) is false.

def SignMatrix.realize {n : ℕ} (A : SignMatrix n) : Matrix (Fin n) (Fin n) ℝ :=
  fun i j => if A i j then -1 else 1

Uses 1 · Used by 7

Statement usesBoolean encoding of sign matrices

Used byAdding the identity to a symmetric conference matrix gives a sign matrix · Boolean matrices realize exactly the sign matrices · Minimum condition number of sign matrices · The minimum condition number is attained · Minimum condition number of order one · The minimum condition number is at least one · Realized sign matrices have entries \(\pm 1\)

TheoremRealized sign matrices have entries \(\pm 1\)#✓fully proved

For every Boolean \(n \times n\) matrix \(A\) and all indices \(i, j\), the \((i, j)\) entry of the real realization of \(A\) is \(1\) or \(-1\).

theorem SignMatrix.realize_entries {n : ℕ} (A : SignMatrix n) (i j : Fin n) :
    A.realize i j = 1 ∨ A.realize i j = -1

Uses 2 · Used by 1

Statement usesBoolean encoding of sign matrices · Real sign matrix of a Boolean matrix

Used byBoolean matrices realize exactly the sign matrices

TheoremBoolean matrices realize exactly the sign matrices#✓fully proved

Send each \(n \times n\) Boolean matrix to the real matrix whose entry is \(-1\) where the Boolean entry is true and \(1\) where it is false. A real \(n \times n\) matrix \(M\) arises in this way if and only if every entry of \(M\) is \(1\) or \(-1\).

theorem exists_realize_iff {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) :
    (∃ A : SignMatrix n, A.realize = M) ↔ ∀ i j, M i j = 1 ∨ M i j = -1

Uses 3 · Used by 1

Statement usesBoolean encoding of sign matrices · Real sign matrix of a Boolean matrix

Proof usesRealized sign matrices have entries \(\pm 1\)

Used byAdding the identity to a symmetric conference matrix gives a sign matrix

DefinitionCondition number of a square real matrix#✓fully proved

For a real \(n \times n\) matrix \(A\), let \(\sigma_0 \ge \sigma_1 \ge \dots\) be the singular values of \(A\) acting on Euclidean space \(\mathbb{R}^n\), indexed from \(0\) and extended by \(\sigma_i = 0\) for \(i \ge n\). The condition number of \(A\), an element of \([0, \infty]\), is \(\infty\) if \(\sigma_{n-1} = 0\) and \(\sigma_0 / \sigma_{n-1}\) otherwise, where \(n - 1\) is read as \(0\) when \(n = 0\).

The minimum over sign matrices is only taken at positive order.

noncomputable def conditionNumber {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ENNReal :=
  let σ := (Matrix.toEuclideanLin A).singularValues
  if σ (n - 1) = 0 then ⊤ else ENNReal.ofReal (σ 0 / σ (n - 1))

Used by 9

Used byCondition number as a singular-value ratio · Infinite condition number from a vanishing singular value · Condition number of the order-one identity · The zero matrix has infinite condition number · Minimum condition number of sign matrices · The minimum condition number is attained · Minimum condition number of order one · Condition numbers are at least one · The minimum condition number is at least one

DefinitionMinimum condition number of sign matrices#✓fully proved

For a positive integer \(n\), the minimum condition number of order \(n\) is the least condition number of a real \(n \times n\) sign matrix, that is, a matrix all of whose entries are \(1\) or \(-1\); the minimum is taken over the finitely many such matrices.

noncomputable def minimumConditionNumber (n : {n : ℕ // 0 < n}) : ENNReal :=
  (Finset.univ : Finset (SignMatrix n.1)).inf' Finset.univ_nonempty
    (fun A => conditionNumber A.realize)

Uses 3 · Used by 4

Statement usesBoolean encoding of sign matrices · Real sign matrix of a Boolean matrix · Condition number of a square real matrix

Used byAdmissible decay exponents · The minimum condition number is attained · Minimum condition number of order one · The minimum condition number is at least one

TheoremInfinite condition number from a vanishing singular value#✓fully proved

Let \(A\) be a real \(n \times n\) matrix with singular values \(\sigma_0 \ge \sigma_1 \ge \dots\) on Euclidean space \(\mathbb{R}^n\), indexed from \(0\) and extended by zeros, where \(n - 1\) is read as \(0\) when \(n = 0\). If \(\sigma_{n-1} = 0\), then the condition number of \(A\) is \(\infty\).

theorem conditionNumber_eq_top_of_smallest_eq_zero {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ)
    (h : (Matrix.toEuclideanLin A).singularValues (n - 1) = 0) :
    conditionNumber A = ⊤

Uses 1

Statement usesCondition number of a square real matrix

TheoremCondition number as a singular-value ratio#✓fully proved

Let \(A\) be a real \(n \times n\) matrix with singular values \(\sigma_0 \ge \sigma_1 \ge \dots\) on Euclidean space \(\mathbb{R}^n\), indexed from \(0\) and extended by zeros, where \(n - 1\) is read as \(0\) when \(n = 0\). If \(\sigma_{n-1} \ne 0\), then the condition number of \(A\) equals \(\sigma_0 / \sigma_{n-1}\).

theorem conditionNumber_eq_ratio_of_smallest_ne_zero {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ)
    (h : (Matrix.toEuclideanLin A).singularValues (n - 1) ≠ 0) :
    conditionNumber A = ENNReal.ofReal
      ((Matrix.toEuclideanLin A).singularValues 0 /
        (Matrix.toEuclideanLin A).singularValues (n - 1))

Uses 1 · Used by 1

Statement usesCondition number of a square real matrix

Used byCondition number of the order-one identity

TheoremThe zero matrix has infinite condition number#✓fully proved

For every natural number \(n\), the condition number of the real \(n \times n\) zero matrix is \(\infty\); this includes the \(0 \times 0\) matrix.

@[simp] theorem conditionNumber_zero (n : ℕ) :
    conditionNumber (0 : Matrix (Fin n) (Fin n) ℝ) = ⊤

Uses 1

Statement usesCondition number of a square real matrix

TheoremThe minimum condition number is attained#✓fully proved

For every positive integer \(n\), there is an \(n \times n\) Boolean matrix whose realization as a real sign matrix (\(-1\) for true, \(1\) for false) has condition number equal to the minimum condition number of order \(n\).

theorem minimumConditionNumber_attained (n : {n : ℕ // 0 < n}) :
    ∃ A : SignMatrix n.1, minimumConditionNumber n = conditionNumber A.realize

Uses 4

Statement usesBoolean encoding of sign matrices · Real sign matrix of a Boolean matrix · Condition number of a square real matrix · Minimum condition number of sign matrices

TheoremCondition numbers are at least one#✓fully proved

For every natural number \(n\) and every real \(n \times n\) matrix \(A\), the condition number of \(A\) is at least \(1\).

theorem one_le_conditionNumber {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
    1 ≤ conditionNumber A

Uses 1 · Used by 1

Statement usesCondition number of a square real matrix

Used byThe minimum condition number is at least one

TheoremThe minimum condition number is at least one#✓fully proved

For every positive integer \(n\), the minimum condition number of the real \(n \times n\) sign matrices is at least \(1\).

theorem one_le_minimumConditionNumber (n : {n : ℕ // 0 < n}) :
    1 ≤ minimumConditionNumber n

Uses 5 · Used by 1

Statement usesMinimum condition number of sign matrices

Proof usesBoolean encoding of sign matrices · Real sign matrix of a Boolean matrix · Condition number of a square real matrix · Condition numbers are at least one

Used byMinimum condition number of order one

TheoremCondition number of the order-one identity#✓fully proved

The condition number of the \(1 \times 1\) real identity matrix is \(1\).

@[simp] theorem conditionNumber_one_order_one :
    conditionNumber (1 : Matrix (Fin 1) (Fin 1) ℝ) = 1

Uses 2 · Used by 1

Statement usesCondition number of a square real matrix

Proof usesCondition number as a singular-value ratio

Used byMinimum condition number of order one

TheoremMinimum condition number of order one#✓fully proved

The minimum condition number of order \(1\) is \(1\): the least condition number of a \(1 \times 1\) real sign matrix is \(1\).

@[simp] theorem minimumConditionNumber_one :
    minimumConditionNumber ⟨1, Nat.zero_lt_one⟩ = 1

Uses 6

Statement usesMinimum condition number of sign matrices

Proof usesBoolean encoding of sign matrices · Real sign matrix of a Boolean matrix · Condition number of a square real matrix · Condition number of the order-one identity · The minimum condition number is at least one

DefinitionSubpolynomial sequences#✓fully proved

A sequence \(f \colon \mathbb{N} \to [0, \infty)\) is subpolynomial when for every real \(\varepsilon > 0\) we have \(f(n) = o(n^{\varepsilon})\) as \(n \to \infty\).

def IsSubpolynomial (f : ℕ → NNReal) : Prop :=
  ∀ ε : ℝ, 0 < ε → IsLittleO atTop (fun n : ℕ => (f n : ℝ))
    (fun n : ℕ => Real.rpow (n : ℝ) ε)

Used by 1

Used byAdmissible decay exponents

DefinitionAdmissible decay exponents#✓fully proved

A real number \(\alpha\) is an admissible exponent when there is a subpolynomial sequence \(f \colon \mathbb{N} \to [0, \infty)\) such that for every positive integer \(n\) the minimum condition number \(\kappa_n\) of the real \(n \times n\) sign matrices satisfies \(\kappa_n = 1 + f(n) / n^{\alpha}\), as an equality in \([0, \infty]\).

def IsAdmissibleExponent (α : ℝ) : Prop :=
  ∃ f : ℕ → NNReal, IsSubpolynomial f ∧
    ∀ (n : ℕ) (hn : 0 < n), minimumConditionNumber ⟨n, hn⟩ =
      1 + (f n : ENNReal) / ENNReal.ofReal (Real.rpow (n : ℝ) α)

Uses 2 · Used by 1

Statement usesSubpolynomial sequences · Minimum condition number of sign matrices

Used byDecay exponent of minimum sign-matrix condition numbers

DefinitionDecay exponent of minimum sign-matrix condition numbers#✓fully proved

The decay exponent is the supremum, taken in the extended reals \([-\infty, \infty]\), of the set of admissible exponents \(\alpha \in \mathbb{R}\).

The supremum need not be attained; it is \(-\infty\) when no exponent is admissible.

noncomputable def decayExponent : EReal :=
  sSup ((fun α : ℝ => (α : EReal)) '' {α : ℝ | IsAdmissibleExponent α})

Uses 1

Statement usesAdmissible decay exponents

DefinitionHadamard hypothesis#✓fully proved

The Hadamard hypothesis is the proposition that for every natural number \(n\) divisible by \(4\) there is an \(n \times n\) Hadamard matrix with integer entries, that is, an integer matrix \(H\) with all entries \(\pm 1\) such that \(H H^{\mathsf{T}} = H^{\mathsf{T}} H = n I\).

This is the Hadamard conjecture, stated as a proposition to be used as a hypothesis.

def HadamardHypothesis : Prop :=
  ∀ n : ℕ, n % 4 = 0 → ∃ M : Matrix (Fin n) (Fin n) ℤ, Matrix.IsHadamard M

DefinitionSymmetric conference matrices#✓fully proved

A real \(n \times n\) matrix \(C\) is a symmetric conference matrix when \(n \ge 2\), \(C^{\mathsf{T}} = C\), every diagonal entry of \(C\) is \(0\), every off-diagonal entry of \(C\) is \(1\) or \(-1\), and \(C C^{\mathsf{T}} = (n - 1) I\), where \(I\) is the identity matrix.

def IsSymmetricConference {n : ℕ} (C : Matrix (Fin n) (Fin n) ℝ) : Prop :=
  2 ≤ n ∧ C.transpose = C ∧ (∀ i, C i i = 0) ∧
    (∀ i j, i ≠ j → C i j = 1 ∨ C i j = -1) ∧
    C * C.transpose = ((n : ℝ) - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)

Used by 1

Used byAdding the identity to a symmetric conference matrix gives a sign matrix

TheoremAdding the identity to a symmetric conference matrix gives a sign matrix#✓fully proved

If \(C\) is a real \(n \times n\) symmetric conference matrix and \(I\) is the \(n \times n\) identity matrix, then there is a Boolean \(n \times n\) matrix whose realization as a real sign matrix equals \(C + I\).

theorem IsSymmetricConference.exists_realize_add_one {n : ℕ}
    {C : Matrix (Fin n) (Fin n) ℝ} (hC : IsSymmetricConference C) :
    ∃ A : SignMatrix n, A.realize = C + 1

Uses 4

Statement usesSymmetric conference matrices · Boolean encoding of sign matrices · Real sign matrix of a Boolean matrix

Proof usesBoolean matrices realize exactly the sign matrices

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.