OAI/NumberTheory/Ostmann/Quadratic/CommonCenterAssembly.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.matchingPrimeSubtype line 12
2. theorem OAI.Ostmann.image_matchingPrimeSubtype line 15
3. theorem OAI.Ostmann.card_matchingPrimeSubtype line 26
4. theorem OAI.Ostmann.card_inter_matchingPrimeSubtype line 31
5. theorem OAI.Ostmann.exists_commonCenter_of_lift_moments line 40

   Source documentation

   The finite form of quad-common-centre-size and quad-common-centre. The only moment assumptions are the explicit counts of integer lifts.

   theorem exists_commonCenter_of_lift_moments (P : Finset ℕ) (N : Finset ℤ)
       (a : ℕ) (ha : 0 < a) (t : ℕ → ℤ) (k d K : ℕ) (hd : d ≤ k + 1)
       (A B L V : ℝ) (hA : 0 < A) (hV : 0 < V)
       (hprime : ∀ p ∈ P, p.Prime) (hap : ∀ p ∈ P, a < p)
       (hlog : ∀ p ∈ P, V ≤ Real.log (p : ℝ))
       (hspan : ∀ n ∈ N, ∀ m ∈ N, n ≠ m →
         Real.log ((n - m).natAbs : ℝ) < (K + 1 : ℕ) * V)
       (hsmall : 2 * K * (P.card : ℝ) ≤ A ^ 2)
       (hlo : (∑ n : N, ((matchingPrimes P a t n.1).card.descFactorial (k + 1 - d) : ℝ)) ≤ B)
       (hhi : L ≤ ∑ n : N, ((matchingPrimes P a t n.1).card.descFactorial (k + 1) : ℝ))
       (hpositive : 0 < L - A ^ d * B) :
       ∃ n ∈ N, ∃ h : ℤ, ∃ m : ℕ,
   …

   Mentions: OAI.Ostmann.matchingPrimes