OAI/NumberTheory/JointDickman/Counting/CoefficientProductSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Nonzero coefficients on the application range are auxiliary-prime products

  1. theorem OAI.JointDickman.coefficientWeight_prime_support line 11
  2. theorem OAI.JointDickman.coefficientWeight_eq_primeProduct line 35
  3. theorem OAI.JointDickman.coefficientWeight_le_scale line 43

    Source documentation

    The elementary global cap used only for the rare common-prime error.

    theorem coefficientWeight_le_scale (B n : ℕ) : coefficientWeight B n ≤ coefficientScale B := by
…

    Mentions: OAI.JointDickman.coefficientWeight, OAI.JointDickman.coefficientScale