Theorems · Theorem · number theory

LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg

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

Defined in: Mathlib.NumberTheory.LSeries.SumCoeff
Cited by: 1 results in Mathlib
Foundations: Depth 279 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.

Cites23

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
Complexstatement · cited by 5,565
nhdsstatement and proof · cited by 5,554
Finset.sumstatement and proof · cited by 5,195
Algebra.algebraMapproof · cited by 4,706
Filter.Tendstostatement and proof · cited by 3,814
Filter.atTopstatement and proof · cited by 2,405
nhdsWithinstatement · cited by 1,912
Complex.ofRealstatement and proof · cited by 1,654
Set.Ioistatement · cited by 1,463
RCLike.ofRealproof · cited by 350
Finset.Iccstatement and proof · cited by 348

Cited by1

Results whose statement or proof uses this declaration.

NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGTproof · cited by 0