OAI/NumberTheory/TwoPointCorrelations/PrimePartialSummation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact partial summation, with the prime-count error retained inside the integral. This is an internal deduction, not an additional published input.

  1. def OAI.TwoPointCorrelations.partialCoefficientSum line 15

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PrimePartialSummation.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.centered_partial_summation line 18

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PrimePartialSummation.lean:18 (same declaration text).

  3. 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/TwoPoint/Bounds/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