Theorems · Theorem · sequences and series
summable_geometric_of_lt_one
∀ {r : ℝ}, 0 ≤ r → r < 1 → Summable fun n => r ^ n- Defined in
- Mathlib.Analysis.SpecificLimits.Basic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- SummationFilter.unconditionalstatement · cited by 2,068
- Summablestatement · cited by 778
- hasSum_geometric_of_lt_oneproof · cited by 14
Cited by19
Results whose statement or proof uses this declaration.
- FormalMultilinearSeries.summable_norm_mul_powproof · cited by 5
- Real.summable_ofDigitsTermproof · cited by 5
- hasSum_geometric_of_norm_lt_oneproof · cited by 4
- Real.ofDigits_le_oneproof · cited by 3
- Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSetproof · cited by 2
- ContinuousLinearMap.exists_preimage_norm_leproof · cited by 2
- hasSum_two_pi_I_cauchyPowerSeries_integralproof · cited by 2
- summable_norm_mul_geometric_of_norm_lt_oneproof · cited by 2
- Cardinal.summable_cantor_functionproof · cited by 2
- ModularForm.multipliableLocallyUniformlyOn_one_sub_powproof · cited by 2
- summable_of_ratio_norm_eventually_leproof · cited by 2
- summable_one_div_pow_of_leproof · cited by 2