OAI/NumberTheory/TwoPoint/Bounds/RandomPrimeRank.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite random-prime rank estimate, manuscript q:rank-probability.

  1. def OAI.TwoPointCorrelations.primeDifference line 15
  2. lemma OAI.TwoPointCorrelations.average_probability_comm line 19
  3. theorem OAI.TwoPointCorrelations.random_prime_rank_squared line 31
  4. theorem OAI.TwoPointCorrelations.random_prime_rank_bound line 110

    Source documentation

    The square-root form of the rank bound.

    theorem random_prime_rank_bound
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
    (B : Matrix ι ι ℤ) (hB : B.det ≠ 0) (f : (ι → P) → ι → ℤ)
    (M : ℕ) (α : ℝ) (hα : 0 ≤ α) (hatom : ∀ p, μ.weight p ≤ α)
    (hsize : ∀ y z : ι → P, ∀ i, (primeDifference P B y z i).natAbs ≤ M) :
    let ν := FiniteLaw.independent (fun _ : ι => μ)
…

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