ZeroRows.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The zero-row estimate used in the random-prime rank lemma.

def OAI.TwoPointCorrelations.rationalRows line 15
lemma OAI.TwoPointCorrelations.rationalRows_surjective line 20
lemma OAI.TwoPointCorrelations.rationalRows_eq_iff line 40

theorem OAI.TwoPointCorrelations.FiniteLaw.zero_rows_probability line 65

Source documentation

Any specified a rows of an invertible integral matrix vanish with probability at most α^a under independent atoms bounded by α.

theorem FiniteLaw.zero_rows_probability
    (μ : ι → FiniteLaw A) (value : A → ℤ) (hvalue : Function.Injective value)
    (B : Matrix ι ι ℤ) (hB : B.det ≠ 0) (S : Finset ι) (y : ι → A)
    (α : ℝ) (hα : 0 ≤ α) (hatom : ∀ i x, (μ i).weight x ≤ α) :
    (FiniteLaw.independent μ).probability (fun x =>
      ∀ i ∈ S, (B *ᵥ ((fun j => value (x j)) - (fun j => value (y j)))) i = 0) ≤
        α ^ S.card := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.probability