OAI/NumberTheory/JointDickman/Amplification/AdditionScaleDichotomy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.addition_product_large_of_not_prefix line 11
2. theorem OAI.JointDickman.addition_scale_dichotomy line 31

   Source documentation

   Either both additions stay in the first three grid cells, or at their first common grid cell one of the products is at least exp(B^(g-1/L)).

   theorem addition_scale_dichotomy {B L : ℕ} (hL : 3 ≤ L) {Z Y : Finset ℕ}
       (hZ : Z ⊆ auxiliaryPrimes B) (hY : Y ⊆ auxiliaryPrimes B) :
       (Z ⊆ primePrefix B ((3 : ℝ)/L) Z ∧ Y ⊆ primePrefix B ((3 : ℝ)/L) Y) ∨
         ∃ k ∈ Icc 4 L,
           Z ⊆ primePrefix B ((k : ℝ)/L) Z ∧ Y ⊆ primePrefix B ((k : ℝ)/L) Y ∧
             (Real.exp ((B : ℝ)^(((k : ℝ)-1)/L)) ≤ (∏ p ∈ Z, p : ℕ) ∨
               Real.exp ((B : ℝ)^(((k : ℝ)-1)/L)) ≤ (∏ p ∈ Y, p : ℕ)) := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primePrefix