PrimePartialSummation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact partial summation, with the prime-count error retained inside the integral.

def OAI.TwoPointCorrelations.partialCoefficientSum line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/PrimePartialSummation.lean:15 (same declaration text).
theorem OAI.TwoPointCorrelations.centered_partial_summation line 18
Also declared: OAI/NumberTheory/TwoPointCorrelations/PrimePartialSummation.lean:18 (same declaration text).

theorem OAI.TwoPointCorrelations.modFive_centered_partial_summation line 63

Source documentation

The same identity for either of the actual modulus-five prime selections.

Also declared: OAI/NumberTheory/TwoPointCorrelations/PrimePartialSummation.lean:63 (same declaration text).

theorem modFive_centered_partial_summation (one : Bool) (a b : ℝ)
    (ha : 0 ≤ a) (hab : a ≤ b) (f : ℝ → ℝ)
    (hf : ∀ x ∈ Set.Icc a b, DifferentiableAt ℝ f x)
    (hdf : ContinuousOn (deriv f) (Set.Icc a b)) :
    (∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f n * modFiveLogWeight one n) -
        modFiveDensity one * (∫ t in a..b, f t) =
      f b * (modFiveTheta one b - modFiveDensity one * b) -
      f a * (modFiveTheta one a - modFiveDensity one * a) -
      ∫ t in a..b, deriv f t * (modFiveTheta one t - modFiveDensity one * t) :=
…

Mentions: OAI.TwoPointCorrelations.modFiveLogWeight, OAI.TwoPointCorrelations.modFiveDensity, OAI.TwoPointCorrelations.modFiveTheta