Theorems · Theorem · sequences and series
hasSum_geometric_of_lt_one
∀ {r : ℝ}, 0 ≤ r → r < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹- Defined in
- Mathlib.Analysis.SpecificLimits.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
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
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- one_mulproof · cited by 2,841
- Filter.atTopproof · cited by 2,405
- SummationFilter.unconditionalstatement · cited by 2,068
- div_eq_mul_invproof · cited by 715
- neg_mulproof · cited by 654
- HasSumstatement · cited by 518
- zero_subproof · cited by 335
- tendsto_const_nhdsproof · cited by 330
- neg_subproof · cited by 272
Cited by14
Results whose statement or proof uses this declaration.
- summable_geometric_of_lt_oneproof · cited by 19
- tsum_geometric_of_lt_oneproof · cited by 6
- hasSum_geometric_two'proof · cited by 4
- aux_hasSum_of_le_geometricproof · cited by 4
- NNReal.hasSum_geometricproof · cited by 3
- hasSum_geometric_twoproof · cited by 2
- HurwitzKernelBounds.F_nat_zero_leproof · cited by 2
- Stirling.log_stirlingSeq_sdiff_le_geo_sumproof · cited by 1
- norm_jacobiTheta_sub_one_leproof · cited by 1
- HurwitzKernelBounds.F_nat_one_leproof · cited by 1
- ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mulproof · cited by 1
- tsum_geometric_le_of_norm_lt_oneproof · cited by 1