CommonCenterCongruences.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Intersections of the matching-prime sets attached to integer lifts

def OAI.Ostmann.matchingPrimes line 14
theorem OAI.Ostmann.matchingPrimes_inter_dvd line 17

theorem OAI.Ostmann.matchingPrimes_inter_card_le line 27

Source documentation

Distinct lifts cannot share more than k large prime congruences.

theorem matchingPrimes_inter_card_le (P : Finset ℕ) (a : ℤ) (t : ℕ → ℤ)
    (n m : ℤ) (hnm : n ≠ m) (k : ℕ) (B : ℝ) (hB : 0 < B)
    (hprime : ∀ p ∈ P, p.Prime) (hlog : ∀ p ∈ P, B ≤ Real.log (p : ℝ))
    (hdiff : Real.log ((n - m).natAbs : ℝ) < (k + 1 : ℕ) * B) :
    (matchingPrimes P a t n ∩ matchingPrimes P a t m).card ≤ k := by
…

Mentions: OAI.Ostmann.matchingPrimes

theorem OAI.Ostmann.matchingPrimes_modEq line 46
Source documentation
A common integer lift determines the same rational center in every matching prime field.
```
theorem matchingPrimes_modEq (P : Finset ℕ) (a : ℤ) (t : ℕ → ℤ) (n : ℤ)
    {p : ℕ} (hp : p ∈ matchingPrimes P a t n) : n ≡ a * t p [ZMOD (p : ℤ)] := by
…
```
Mentions: OAI.Ostmann.matchingPrimes