OAI/NumberTheory/Ostmann/Construction/OriginalTupleLifts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.int_mem_symmetric_Ico_of_abs_le line 15
2. theorem OAI.Ostmann.eventual_original_tuple_witness_lift line 25

   Source documentation

   Apply the inverse phase theorem to the literal small-kernel event.

   theorem eventual_original_tuple_witness_lift (B : ℝ) (Φ : 𝓢(ℝ, ℂ))
       (hB : 3 ≤ B) (hΦ : ∀ x : ℝ, B ^ 2 < x → Φ x = 0) :
       ∀ᶠ T : ℝ in atTop, ∀ (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
         (D : ∀ p : ℕ, Finset (ZMod p)) (P : Finset ℕ) (_hP : ∀ p ∈ P, p.Prime)
         (k N : ℕ) (t τ : ℕ → ℤ) (h₀ : ℕ → ℕ) (X : ℝ),
         0 < X → (Q.toList.prod : ℝ) ≤ Real.exp (T / 50) →
         (Q.card : ℝ) ≤ T ^ (9999999 / 10000000 : ℝ) →
         (∀ m ∈ primeSubsetProducts P k,
           Real.exp (10 * T) ≤ (m : ℝ) / X ∧ (m : ℝ) / X ≤ Real.exp (14 * T) ∧
           ∀ p ∈ m.primeFactors, (p : ℤ) ∣ τ m - t p) →
         ∀ e : Fin k ↪ P,
           principalSmallWitness Q hQ D (primeTupleProduct P e) N (h₀ (primeTupleProduct P e))
   …

   Mentions: OAI.Ostmann.primeSubsetProducts, OAI.Ostmann.principalSmallWitness, OAI.Ostmann.primeTupleProduct

3. def OAI.Ostmann.tupleLiftFamily line 56
4. theorem OAI.Ostmann.primeTuple_event_probability line 60
5. theorem OAI.Ostmann.tupleLiftFamily_probability line 68