Theorems · Theorem · number theory

LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div

∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l) →
    (∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s) →
      Filter.Tendsto (fun s => (↑s - 1) * LSeries f ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds l)

Defined in: Mathlib.NumberTheory.LSeries.SumCoeff
Cited by: 1 results in Mathlib
Foundations: Depth 278 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites47

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
Filterproof · cited by 8,121
Complexstatement and proof · cited by 5,565
nhdsstatement and proof · cited by 5,554
Norm.normproof · cited by 5,413
Finset.sumstatement and proof · cited by 5,195
Filter.Tendstostatement and proof · cited by 3,814
Nat.cast_oneproof · cited by 2,501
Filter.atTopstatement and proof · cited by 2,405
zero_addproof · cited by 2,366
nhdsWithinstatement and proof · cited by 1,912

Cited by1

Results whose statement or proof uses this declaration.

LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonnegproof · cited by 1