OAI/NumberTheory/TwoPoint/Bounds/SmoothReciprocalMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-prime smooth reciprocal sums. The exact Euler factors make averaging the dilation cost against the padding law possible.

  1. def OAI.TwoPointCorrelations.smoothReciprocalProduct line 15
  2. def OAI.TwoPointCorrelations.natNegativePower line 18
  3. lemma OAI.TwoPointCorrelations.smoothReciprocalProduct_hasSum line 25
  4. lemma OAI.TwoPointCorrelations.smoothReciprocalProduct_nonneg line 37
  5. lemma OAI.TwoPointCorrelations.smooth_reciprocal_sum_le line 44
  6. lemma OAI.TwoPointCorrelations.smooth_divisor_reciprocal_sum_le line 62

    Source documentation

    The geometric reciprocal cost of every smooth part of a bounded integer is controlled independently of the outer bound.

    lemma smooth_divisor_reciprocal_sum_le (q n : ℕ) (s : ℝ) (hs : 0 < s) :
    (∑ a ∈ n.divisors.filter (fun a => a.primeFactors ⊆ q.primeFactors),
      (a : ℝ) ^ (-s)) ≤ smoothReciprocalProduct q.primeFactors s := by
…

    Mentions: OAI.TwoPointCorrelations.smoothReciprocalProduct