OAI/NumberTheory/JointDickman/Arithmetic/RegularPrimeSets.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.auxiliaryLogLength line 13
2. def OAI.JointDickman.primePrefix line 15
3. def OAI.JointDickman.primeTailEndpoint line 18
4. def OAI.JointDickman.RegularPrimeSet line 23

   Source documentation

   The last dyadic endpoint and all later endpoints impose an automatic condition when C is nonnegative, so the tail condition is stated for all i.

   def RegularPrimeSet (B L : ℕ) (τ C : ℝ) (S : Finset ℕ) : Prop :=
   …

5. def OAI.JointDickman.coefficientPrimeSet line 31
6. def OAI.JointDickman.residueBaseWeight line 34
7. def OAI.JointDickman.regularResidueWeight line 38
8. def OAI.JointDickman.regularCoefficientWeight line 42
9. theorem OAI.JointDickman.RegularPrimeSet.total_lower line 45
10. theorem OAI.JointDickman.residueBaseWeight_le_of_count line 52
11. theorem OAI.JointDickman.regularResidueWeight_nonneg line 67
12. theorem OAI.JointDickman.regularCoefficientWeight_nonneg line 74
13. theorem OAI.JointDickman.coefficientWeight_le_residueBaseWeight line 81
14. theorem OAI.JointDickman.coefficientPrimeSet_eq_inter line 108

    Source documentation

    On nonzero integers the dividing-prime set is exactly the intersection with the integer's finite prime-factor set.

    theorem coefficientPrimeSet_eq_inter {B n : ℕ} (hn : n ≠ 0) :
        coefficientPrimeSet B n = n.primeFactors ∩ auxiliaryPrimes B := by
    …

    Mentions: OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.auxiliaryPrimes

15. theorem OAI.JointDickman.primePrefix_inter line 119