OAI/NumberTheory/JointDickman/Amplification/WeightedPartialSummation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.weighted_counting_error_le line 14

   Source documentation

   A C¹ test loses only its value and first-derivative bounds when a summatory estimate is transferred to a weighted sum.

   theorem weighted_counting_error_le (w : ℕ → ℝ) (F φ φ' : ℝ → ℝ)
       {a b ε M N : ℝ} (ha : 0 ≤ a) (hab : a ≤ b)
       (hε : 0 ≤ ε) (hM : 0 ≤ M) (hN : 0 ≤ N)
       (hφ : ∀ t ∈ Set.Icc a b, HasDerivAt φ (φ' t) t)
       (hφ' : ContinuousOn φ' (Set.Icc a b)) (hF : ContinuousOn F (Set.Icc a b))
       (hvalue : ∀ t ∈ Set.Icc a b, |φ t| ≤ M)
       (hderiv : ∀ t ∈ Set.Icc a b, |φ' t| ≤ N)
       (herr : ∀ t ∈ Set.Icc a b, |finiteCountingFunction w t - F t| ≤ ε * t) :
       |(∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, φ n * w n) -
         (φ b * F b - φ a * F a - ∫ t in a..b, φ' t * F t)| ≤
         ε * b * (2 * M + N * (b - a)) := by
   …

   Mentions: OAI.JointDickman.finiteCountingFunction