Singularity of random Bernoulli matrices | Lean AI formalization leaderboard

Problem statement

Notes: The proof binders `mΩ`, `B_indep`, and `B_bernoulli` in `theorem_A` are prefixed with `_` here. This is alpha-equivalent and suppresses unused-variable warnings in the generated `Solution.lean` delegation.

Source: K. Tikhomirov, `Singularity of random Bernoulli matrices`, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-191-2-RandomBernoulliMatrices.lean

Informal solution: Unavailable.

/--
Statement of Theorem A:

For every `p ∈ (0, 1/2]` and `ε > 0` there exists `N, C > 0` such that for any `n ≥ N` and any
`n × n` random matrix `B` with mutually independent `Bernoulli(p)` entries,

`P(σ_min (B + sIIᵀ) ≤ t/√n) ≤ (1 - p + ε)ⁿ + Ct` for all `s ∈ [-1,0]` and `t > 0`.
-/
theorem declaration uses `sorry`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 := byp:↑Iε:ℝhp₀:0 < php₁:↑p ≤ 1 / 2hε:0 < ε⊢ ∃ N > 0,
  ∃ C > 0,
    ∀ n ≥ N,
      ∀ (Ω : Type u_1) (_mΩ : MeasurableSpace Ω) (P : Measure Ω) (B : Ω → Matrix (Fin n) (Fin n) ℝ),
        iIndepFun (fun x x_1 => B x_1 x.1 x.2) P →
          (∀ (i j : Fin n), HasLaw (fun x => B x i j) Ber(1, 0, p) P) →
            ∀ (s : ℝ),
              -1 ≤ s ∧ s ≤ 0 →
                ∀ (t : ℝ), 0 < t → P.real {ω | σ_min (B ω + of fun x x_1 => s) ≤ t / √↑n} ≤ (1 - ↑p + ε) ^ n + C * t
  sorryAll goals completed! 🐙

/--
This (unnamed) corollary appears directly below Theorem A in the paper:

For every `p ∈ (0, 1/2]` and any sequence `Bₙ` of `n × n` random matrices with mutually
independent `Bernoulli(p)` entries we have that

`P(Bₙ is singular) = (1 - p + oₙ(1))ⁿ`.
-/
theorem declaration uses `sorry`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 := byp:↑Ihp₀:0 < php₁:↑p ≤ 1 / 2Ω:ℕ → Type u_1mΩ:(n : ℕ) → MeasurableSpace (Ω n)P:(n : ℕ) → Measure (Ω n)B:(n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝB_indep:∀ (n : ℕ), iIndepFun (fun x x_1 => B n x_1 x.1 x.2) (P n)B_bernoulli:∀ (n : ℕ) (i j : Fin n), HasLaw (fun x => B n x i j) Ber(1, 0, p) (P n)⊢ ∃ o, o =o[atTop] 1 ∧ ∀ n > 0, (P n).real {ω | (B n ω).det = 0} = (1 - ↑p + o n) ^ n
  sorryAll goals completed! 🐙

/--
This is the result stated in the paper's abstract:

For any sequence `Mₙ` of `n × n` random matrices with mutually independent `Rademacher` entries
we have that

`P(Mₙ is singular) = (1/2 + oₙ(1))ⁿ`.
-/
theorem declaration uses `sorry`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 := byΩ:ℕ → Type u_1mΩ:(n : ℕ) → MeasurableSpace (Ω n)P:(n : ℕ) → Measure (Ω n)M:(n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝM_indep:∀ (n : ℕ), iIndepFun (fun x x_1 => M n x_1 x.1 x.2) (P n)M_rademacher:∀ (n : ℕ) (i j : Fin n), HasLaw (fun x => M n x i j) rademacherMeasure (P n)⊢ ∃ o, o =o[atTop] 1 ∧ ∀ n > 0, (P n).real {ω | (M n ω).det = 0} = (1 / 2 + o n) ^ n
  sorryAll goals completed! 🐙