HighRankColumns.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The selected high-rank congruences under the full product prime law.

theorem OAI.TwoPointCorrelations.full_coordinate_prime_rank_bound line 16

Source documentation

Outside variables are truly integrated, rather than conditioned away. Repeated numerical primes remain allowed by the independent product law.

theorem full_coordinate_prime_rank_bound
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
    (w : ρ → α → ℤ) (control pivot : ρ → α)
    (hc : Function.Injective control) (hp : Function.Injective pivot)
    (hdisjoint : ∀ i j, pivot i ≠ control j)
    (hdet : (Matrix.of fun i j => w i (pivot j)).det ≠ 0)
    (M : ℕ) (a : ℝ) (ha : 0 ≤ a) (hatom : ∀ p, μ.weight p ≤ a)
    (hsize : ∀ y z : ρ → P, ∀ i,
      (primeDifference P (fun i j => w i (pivot j)) y z i).natAbs ≤ M) :
    (FiniteLaw.independent (fun _ : α => μ)).probability (fun x =>
      ∀ i, ((x (control i)).val : ℤ) ∣ ∑ z, w i z * ((x z).val : ℤ)) ≤
      Real.sqrt ((a * (1 + (Nat.log 2 M : ℝ))) ^ Fintype.card ρ) := by
…

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

theorem OAI.TwoPointCorrelations.independent_pairs_prime_rank_bound line 57

Source documentation

Jointly independent difference/control pairs supply all algebraic premises of the full-coordinate probability bound.

theorem independent_pairs_prime_rank_bound
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
    (w : ρ → α → ℤ) (control : ρ → α)
    (hind : LinearIndependent ℝ (Sum.elim (fun i z => (w i z : ℝ))
      (fun i => Pi.basisFun ℝ α (control i))))
    (M : ℕ) (a : ℝ) (ha : 0 ≤ a) (hatom : ∀ p, μ.weight p ≤ a)
    (hsize : ∀ pivot : ρ → α, Function.Injective pivot →
      (∀ i j, pivot i ≠ control j) → ∀ y z : ρ → P, ∀ i,
      (primeDifference P (fun i j => w i (pivot j)) y z i).natAbs ≤ M) :
    (FiniteLaw.independent (fun _ : α => μ)).probability (fun x =>
      ∀ i, ((x (control i)).val : ℤ) ∣ ∑ z, w i z * ((x z).val : ℤ)) ≤
      Real.sqrt ((a * (1 + (Nat.log 2 M : ℝ))) ^ Fintype.card ρ) := by
…

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