OAI/NumberTheory/TwoPoint/Bounds/SmoothDivisorDecomposition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact decomposition along primes of a fixed dilation. The coefficient of a smooth divisor is bounded by one; there is no signed local expansion or factor exponential in the number of dilation primes.

  1. def OAI.TwoPointCorrelations.primeSmoothPart line 17
  2. def OAI.TwoPointCorrelations.primeRoughPart line 20
  3. lemma OAI.TwoPointCorrelations.primeSmoothPart_mul_primeRoughPart line 23
  4. lemma OAI.TwoPointCorrelations.primeSmoothPart_pos line 29
  5. lemma OAI.TwoPointCorrelations.primeRoughPart_pos line 34
  6. lemma OAI.TwoPointCorrelations.primeSmoothPart_support line 39
  7. lemma OAI.TwoPointCorrelations.primeRoughPart_coprime line 50
  8. lemma OAI.TwoPointCorrelations.coprime_of_primeFactors_subset line 61
  9. lemma OAI.TwoPointCorrelations.primeSmoothPart_unique line 70
  10. def OAI.TwoPointCorrelations.coprimeRestriction line 87
  11. lemma OAI.TwoPointCorrelations.coprimeRestriction_oneBounded line 90
  12. lemma OAI.TwoPointCorrelations.coprimeRestriction_multiplicative line 98
  13. lemma OAI.TwoPointCorrelations.coprimeRestriction_prime line 112
  14. theorem OAI.TwoPointCorrelations.multiplicative_dilation_smooth_sum line 123

    Source documentation

    The fixed-dilation sequence is a positive-density convolution over smooth divisors; its scalar coefficients have modulus at most one.

    theorem multiplicative_dilation_smooth_sum {f : ℕ → ℂ} (hf : Multiplicative f)
    (q n : ℕ) (hq : 0 < q) (hn : 0 < n) :
    f (q * n) = ∑ a ∈ n.divisors.filter (fun a => a.primeFactors ⊆ q.primeFactors),
      f (q * a) * coprimeRestriction q f (n / a) := by
…

    Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.coprimeRestriction