Singularity of random Bernoulli matrices

DefinitionSmallest singular value of a matrix#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(M\) be a matrix over \(\mathbb{K}\) whose rows and columns are indexed by finite sets \(n\) and \(m\). Its smallest singular value is the real number \(\sigma_{\min}(M) = \inf_{x \in \mathbb{K}^m,\ \lVert x \rVert_2 = 1} \lVert Mx \rVert_2\), where \(\lVert \cdot \rVert_2\) is the Euclidean norm. When \(m\) is empty there are no unit vectors, and \(\sigma_{\min}(M) = 0\).

noncomputable def σ_min {𝕜 n m : Type*} [Fintype n] [Fintype m] [DecidableEq m]
    [RCLike 𝕜] (M : Matrix n m 𝕜) :=
  ⨅ x : {x : EuclideanSpace 𝕜 m // ‖x‖ = 1}, ‖M.toEuclideanLin x‖

Used by 1

Used byTikhomirov's Theorem A: smallest singular value of shifted Bernoulli matrices

DefinitionRademacher measure on the real line#✓fully proved

The Rademacher measure is the probability measure on \(\mathbb{R}\) that assigns mass \(1/2\) to \(1\) and mass \(1/2\) to \(-1\).

noncomputable def rademacherMeasure : Measure ℝ :=
  bernoulliMeasure 1 (-1) ⟨1 / 2, by norm_num⟩

Used by 1

Used bySingularity probability of Rademacher matrices

TheoremTikhomirov's Theorem A: smallest singular value of shifted Bernoulli matrices#●ready to prove

Let \(0 < p \le 1/2\) and \(\varepsilon > 0\), and write \(\sigma_{\min}(A)\) for the smallest singular value of a real square matrix \(A\). There exist a natural number \(N > 0\) and a real number \(C > 0\) such that for every \(n \ge N\) the following holds. Let \(B\) be a random \(n \times n\) real matrix on a probability space \((\Omega, P)\) whose \(n^2\) entries are mutually independent and each equal to \(1\) with probability \(p\) and to \(0\) with probability \(1 - p\), and let \(J\) be the \(n \times n\) matrix all of whose entries are \(1\). Then for every \(s \in [-1, 0]\) and every real \(t > 0\),

\[P\bigl(\sigma_{\min}(B + sJ) \le t / \sqrt{n}\bigr) \le (1 - p + \varepsilon)^n + C t.\]

public theorem_wanted theorem_A {p : I} {ε : ℝ} (hp₀ : 0 < p) (hp₁ : (p : ℝ) ≤ 1 / 2) (hε : 0 < ε) :
    ∃ N > 0, ∃ C > 0, ∀ n ≥ N,
      ∀ (Ω : Type*) (_mΩ : MeasurableSpace Ω) (P : Measure Ω) (B : Ω → Matrix (Fin n) (Fin n) ℝ)
        (_B_indep : iIndepFun (fun x : Fin n × Fin n ↦ (B · x.1 x.2)) P)
        (_B_bernoulli : ∀ i j, HasLaw (B · i j) (bernoulliMeasure 1 0 p) P),
        ∀ s : ℝ, -1 ≤ s ∧ s ≤ 0 → ∀ t : ℝ, 0 < t →
          P.real {ω : Ω | σ_min (B ω + of (fun _ _ ↦ s)) ≤ t / √n} ≤ (1 - p + ε) ^ n + C * t

Sources

• K. Tikhomirov, Singularity of random Bernoulli matrices, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_random_bernoulli_matrices of the lean-eval benchmark.

Uses 1

Statement usesSmallest singular value of a matrix

TheoremSingularity probability of Bernoulli matrices#●ready to prove

Let \(0 < p \le 1/2\). For each \(n\), let \(B_n\) be a random \(n \times n\) real matrix on a probability space \((\Omega_n, P_n)\) whose \(n^2\) entries are mutually independent and each equal to \(1\) with probability \(p\) and to \(0\) with probability \(1 - p\). Then there is a function \(o : \mathbb{N} \to \mathbb{R}\) with \(o(n) \to 0\) as \(n \to \infty\) such that \(P_n(\det B_n = 0) = (1 - p + o(n))^n\) for every \(n \ge 1\).

public theorem_wanted corollary_1 {p : I} (hp₀ : 0 < p) (hp₁ : (p : ℝ) ≤ 1 / 2)
    {Ω : ℕ → Type*} [mΩ : ∀ n, MeasurableSpace (Ω n)] {P : (n : ℕ) → Measure (Ω n)}
    {B : (n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝ}
    (B_indep : ∀ n, iIndepFun (fun x : Fin n × Fin n ↦ (B n · x.1 x.2)) (P n))
    (B_bernoulli : ∀ n i j, HasLaw (B n · i j) (bernoulliMeasure 1 0 p) (P n)) :
    ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
      ∀ n > 0, (P n).real {ω | (B n ω).det = 0} = (1 - p + o n) ^ n

Sources

• K. Tikhomirov, Singularity of random Bernoulli matrices, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_random_bernoulli_matrices of the lean-eval benchmark.

TheoremSingularity probability of Rademacher matrices#●ready to prove

For each \(n\), let \(M_n\) be a random \(n \times n\) real matrix on a probability space \((\Omega_n, P_n)\) whose \(n^2\) entries are mutually independent and each have the Rademacher law, with mass \(1/2\) at each of \(1\) and \(-1\). Then there is a function \(o : \mathbb{N} \to \mathbb{R}\) with \(o(n) \to 0\) as \(n \to \infty\) such that \(P_n(\det M_n = 0) = (1/2 + o(n))^n\) for every \(n \ge 1\).

public theorem_wanted corollary_2 {Ω : ℕ → Type*} (mΩ : ∀ n, MeasurableSpace (Ω n)) {P : (n : ℕ) → Measure (Ω n)}
    {M : (n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝ}
    (M_indep : ∀ n, iIndepFun (fun x : Fin n × Fin n ↦ (M n · x.1 x.2)) (P n))
    (M_rademacher : ∀ n i j, HasLaw (M n · i j) rademacherMeasure (P n)) :
    ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
      ∀ n > 0, (P n).real {ω | (M n ω).det = 0} = (1 / 2 + o n) ^ n

Sources

• K. Tikhomirov, Singularity of random Bernoulli matrices, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_random_bernoulli_matrices of the lean-eval benchmark.

Uses 1

Statement usesRademacher measure on the real line

2 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.