OAI/NumberTheory/TwoPoint/Bounds/SievePrimeSubsets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Products of prime subsets realize distinct terms of the finite sieve denominator.

  1. lemma OAI.TwoPointCorrelations.sieve_prime_subset_squarefree line 13
  2. lemma OAI.TwoPointCorrelations.sieve_prime_subset_injective line 22
  3. lemma OAI.TwoPointCorrelations.sieve_prime_subset_weight line 32
  4. lemma OAI.TwoPointCorrelations.sieve_prime_subset_log line 40
  5. theorem OAI.TwoPointCorrelations.sieve_prime_subset_denominator line 48

    Source documentation

    A truncated prime-subset Euler product is a genuine subsum of the actual Goldbach denominator.

    theorem sieve_prime_subset_denominator (N z : ℕ) (hN : 2 ∣ N)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) :
    (∑ T ∈ P.powerset with (∏ p ∈ T, p) ≤ z, ∏ p ∈ T, sieveGoldbachWeight N p) ≤
      GoldbachSelberg.denominator N (primorial z) z := by
…

    Mentions: OAI.TwoPointCorrelations.sieveGoldbachWeight