OAI/NumberTheory/JointDickman/Arithmetic/PrimeHarmonicWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.primeProduct_squarefree line 17
2. theorem OAI.JointDickman.primeProduct_cardFactors line 24
3. theorem OAI.JointDickman.uncorrectedSubsetMass_harmonic line 36
4. def OAI.JointDickman.uncorrectedPrimeProductMass line 49
5. theorem OAI.JointDickman.uncorrectedPrimeProductMass_at_product line 53
6. theorem OAI.JointDickman.uncorrectedPrimeProductMass_eq_zero line 67
7. theorem OAI.JointDickman.uncorrectedPrimeProductMass_harmonic line 76
8. theorem OAI.JointDickman.primeProductMass_sum_event line 112
9. theorem OAI.JointDickman.uncorrectedPrimeProductMass_sum_event line 123
10. theorem OAI.JointDickman.primeProductMass_harmonic_error line 135

    Source documentation

    The probability of any bounded set differs from its harmonic rough weight by at most the reciprocal-square prime tail.

    theorem primeProductMass_harmonic_error {U : ℝ} {N : ℕ} (hN : N ≠ 0)
        {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1) (K : Finset ℕ)
        (hK : ∀ n ∈ K, (n : ℝ) ≤ U) :
        |(∑ n ∈ K, primeProductMass (largePrimeSet U N) z n) -
          primeNormalizer (largePrimeSet U N) z *
            ∑ n ∈ K, roughSquarefreeWeight (Nat.primesLE N) z n / n| ≤ z ^ 2 / (N : ℝ) := by
    …

    Mentions: OAI.JointDickman.primeProductMass, OAI.JointDickman.largePrimeSet, OAI.JointDickman.primeNormalizer, OAI.JointDickman.roughSquarefreeWeight