Theorems · Theorem · number theory

tendsto_sum_mul_atTop_nhds_one_sub_integral

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

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