OAI/NumberTheory/TwoPoint/Bounds/PrimeSubsetSplitting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.primeSubset_products_coprime line 15
2. lemma OAI.TwoPointCorrelations.retainedPrimeDivisors_avoiding line 33
3. lemma OAI.TwoPointCorrelations.nonrawRoughSupport_of_primeSubset line 59
4. lemma OAI.TwoPointCorrelations.primeSubset_core_retained line 71
5. theorem OAI.TwoPointCorrelations.nonraw_subset_sum line 82

   Source documentation

   The removed-subset sum is exactly the numerical rough-support sum, including its reciprocal coefficient and the prime-factor exponent.

   theorem nonraw_subset_sum (U T : Finset ℕ)
       (hU : ∀ p ∈ U, Nat.Prime p) (hT : ∀ p ∈ T, Nat.Prime p)
       (H τ : ℝ) (θ : ℂ) (F : ℕ → ℂ) :
       (∑ W ∈ (T \ U).powerset,
         if 1 < (∏ p ∈ W, p) ∧ H < (((∏ p ∈ U, p) * (∏ p ∈ W, p) : ℕ) : ℝ) ∧
             (((∏ p ∈ U, p) * (∏ p ∈ W, p) : ℕ) : ℝ) ≤ τ * H
         then ((-θ) ^ W.card / ((∏ p ∈ W, p : ℕ) : ℂ)) * F (∏ p ∈ W, p)
         else 0) =
         ∑ w ∈ nonrawRoughSupport T H τ (∏ p ∈ U, p),
           ((-θ) ^ w.primeFactors.card / (w : ℂ)) * F w := by
   …

   Mentions: OAI.TwoPointCorrelations.nonrawRoughSupport