ReciprocalProgressions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal savings for one prime variable in a nondegenerate congruence.

theorem OAI.TwoPointCorrelations.reciprocal_congruence_sum line 17

Source documentation

A finite subset of one residue class has at most one exceptional initial term; every subsequent reciprocal is bounded by a harmonic term divided by the modulus. The set may consist only of primes or satisfy extra restrictions.

theorem reciprocal_congruence_sum (S : Finset ℕ) (H N p : ℕ)
    (hH : 0 < H) (hN : 1 ≤ N) (hp : 0 < p)
    (hlower : ∀ x ∈ S, H ≤ x) (hupper : ∀ x ∈ S, x ≤ N)
    (hcongruent : ∀ x ∈ S, ∀ y ∈ S, Nat.ModEq p x y) :
    ∑ x ∈ S, (x : ℝ)⁻¹ ≤ (H : ℝ)⁻¹ + (1 + Real.log N) / p := by
…

lemma OAI.TwoPointCorrelations.congruence_same_residue line 90
Source documentation
A congruence with a nonzero coefficient modulo a prime admits only one residue class, without any assumption that a larger matrix is invertible.
```
lemma congruence_same_residue {p x y : ℕ} (hp : p.Prime) {A B : ℤ}
    (hA : ¬(p : ℤ) ∣ A)
    (hx : (p : ℤ) ∣ A * x + B) (hy : (p : ℤ) ∣ A * y + B) :
    Nat.ModEq p x y := by
…
```

theorem OAI.TwoPointCorrelations.reciprocal_linear_congruence_sum line 101

Source documentation

The reciprocal saving used for each selected triangular relation.

theorem reciprocal_linear_congruence_sum (S : Finset ℕ) (H N p : ℕ) (A B : ℤ)
    (hH : 0 < H) (hN : 1 ≤ N) (hp : p.Prime) (hA : ¬(p : ℤ) ∣ A)
    (hlower : ∀ x ∈ S, H ≤ x) (hupper : ∀ x ∈ S, x ≤ N)
    (hcongruence : ∀ x ∈ S, (p : ℤ) ∣ A * x + B) :
    ∑ x ∈ S, (x : ℝ)⁻¹ ≤ (H : ℝ)⁻¹ + (1 + Real.log N) / p := by
…