OAI/NumberTheory/JointDickman/Counting/CoefficientDyadicBoxes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.coefficientDyadicBox line 13
2. def OAI.JointDickman.coefficientDyadicCover line 16
3. theorem OAI.JointDickman.coefficientDyadicBox_disjoint line 19
4. def OAI.JointDickman.amplificationCoefficientPairs line 36
5. theorem OAI.JointDickman.nat_two_pow_exp line 41
6. theorem OAI.JointDickman.coefficientDyadicCover_contains line 46
7. theorem OAI.JointDickman.mem_amplificationCoefficientPairs line 83
8. theorem OAI.JointDickman.coefficientDyadicBox_scales line 95

   Source documentation

   Every box in the cover is long enough for the sieve and remains inside the coefficient range of the local prime-product law.

   theorem coefficientDyadicBox_scales :
       ∀ᶠ B : ℕ in atTop, ∀ T k : ℕ, (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
         k ∈ Ico B (4 * B) →
         Real.exp ((1 / 2 : ℝ) * B) ≤ ((2^k : ℕ) : ℝ) ∧
           (4 * T * (2^k : ℕ) : ℝ) ≤ Real.exp ((16 / 5 : ℝ) * B) := by
   …

9. theorem OAI.JointDickman.amplificationCoefficientPairs_size line 131