OAI/NumberTheory/JointDickman/Arithmetic/PrimeSubsetTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cutoff tails for the squarefree divisor expansion

  1. def OAI.JointDickman.primeSubsetTail line 9
  2. theorem OAI.JointDickman.primeSubsetTail_degree_le line 15
  3. theorem OAI.JointDickman.primeSubsetTail_sum_degree line 32
  4. theorem OAI.JointDickman.primeSubsetTail_bound line 57

    Source documentation

    Only finitely many degrees occur when every prime exceeds a fixed positive power of the cutoff. No distinctness estimate is needed here.

    theorem primeSubsetTail_bound : ∃ C : ℝ, 0 ≤ C ∧
    ∀ (P : Finset ℕ) (J : ℕ) (y Y N : ℝ), 2 ≤ y → 1 ≤ Y → Y ≤ N →
      (∀ p ∈ P, p.Prime ∧ y < (p:ℝ)) →
      (∀ D ∈ P.powerset, (∏ p ∈ D, (p:ℝ)) ≤ N → D.card ≤ J) →
      primeSubsetTail P Y N ≤ ((Real.log (N/Y)+C)/Real.log y)*
        ∑ h ∈ range J, (∑ p ∈ P, 1/(p:ℝ))^h := by
…

    Mentions: OAI.JointDickman.primeSubsetTail