Theorems · Theorem · number theory

summable_mul_of_bigO_atTop

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  (∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x => ‖f x‖) t) →
    MeasureTheory.LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 0) MeasureTheory.volume →
      ((fun n => ‖f ↑n‖ * ∑ k ∈ Finset.Icc 0 n, ‖c k‖) =O[Filter.atTop] fun x => 1) →
        ∀ {g : ℝ → ℝ},
          (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, ‖c k‖) =O[Filter.atTop] g →
            MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume → Summable fun n => f ↑n * c n

Defined in

Mathlib.NumberTheory.AbelSummation

Cited by

0 results in Mathlib

Foundations

Depth 273 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLike