Normed

📁 Source: Mathlib/Analysis/SpecificLimits/Normed.lean

Statistics

Metric	Count
Definitions `HasSummableGeomSeries`, `oneSub`	2
Theorems `tendsto_div_one_add_pow_nhds_one`, `tendsto_div_one_add_pow_nhds_zero`, `alternating_series_le_tendsto`, `cauchySeq_alternating_series_of_tendsto_zero`, `cauchySeq_series_mul_of_tendsto_zero_of_bounded`, `tendsto_alternating_series_of_tendsto_zero`, `tendsto_le_alternating_series`, `summable_geometric_of_norm_lt_one`, `alternating_series_le_tendsto`, `cauchySeq_alternating_series_of_tendsto_zero`, `cauchySeq_series_mul_of_tendsto_zero_of_bounded`, `tendsto_alternating_series_of_tendsto_zero`, `tendsto_le_alternating_series`, `cauchy_series_of_le_geometric'`, `cauchy_series_of_le_geometric''`, `summable_pow_div_factorial`, `cauchySeq_of_le_geometric`, `tendsto_alternating_series_tsum`, `TFAE_exists_lt_isLittleO_pow`, `val_oneSub`, `alternating_series_error_bound`, `cauchySeq_finset_of_geometric_bound`, `cauchy_series_of_le_geometric`, `dist_partial_sum`, `dist_partial_sum'`, `dist_partial_sum_le_of_le_geometric`, `exists_norm_le_of_cauchySeq`, `geom_series_eq_inverse`, `geom_series_mul_neg`, `geom_series_mul_one_add`, `geom_series_mul_shift`, `geom_series_succ`, `hasSum_choose_mul_geometric_of_norm_lt_one`, `hasSum_choose_mul_geometric_of_norm_lt_one'`, `hasSum_coe_mul_geometric_of_norm_lt_one`, `hasSum_coe_mul_geometric_of_norm_lt_one'`, `hasSum_geom_series_inverse`, `hasSum_geometric_of_abs_lt_one`, `hasSum_geometric_of_norm_lt_one`, `instHasSummableGeomSeries`, `instHasSummableGeomSeriesOfCompleteSpace`, `isBigO_pow_pow_of_le_left`, `isLittleO_coe_const_pow_of_one_lt`, `isLittleO_pow_const_const_pow_of_one_lt`, `isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt`, `isLittleO_pow_pow_of_abs_lt_left`, `isLittleO_pow_pow_of_lt_left`, `isUnit_one_sub_of_norm_lt_one`, `mul_neg_geom_series`, `norm_sub_le_of_geometric_bound_of_hasSum`, `norm_sum_neg_one_pow_le`, `not_summable_of_ratio_norm_eventually_ge`, `not_summable_of_ratio_test_tendsto_gt_one`, `summable_choose_mul_geometric_of_norm_lt_one`, `summable_descFactorial_mul_geometric_of_norm_lt_one`, `summable_geometric_iff_norm_lt_one`, `summable_geometric_of_abs_lt_one`, `summable_geometric_of_norm_lt_one`, `summable_norm_geometric_of_norm_lt_one`, `summable_norm_mul_geometric_of_norm_lt_one`, `summable_norm_pow_mul_geometric_of_norm_lt_one`, `summable_of_ratio_norm_eventually_le`, `summable_of_ratio_test_tendsto_lt_one`, `summable_pow_mul_geometric_of_norm_lt_one`, `summable_powerSeries_of_norm_lt`, `summable_powerSeries_of_norm_lt_one`, `tendsto_const_div_pow`, `tendsto_intCast_atBot_cobounded`, `tendsto_intCast_atBot_sup_atTop_cobounded`, `tendsto_intCast_atTop_cobounded`, `tendsto_natCast_atTop_cobounded`, `tendsto_pow_atTop_nhds_zero_iff_norm_lt_one`, `tendsto_pow_atTop_nhds_zero_of_abs_lt_one`, `tendsto_pow_atTop_nhds_zero_of_norm_lt_one`, `tendsto_pow_const_div_const_pow_of_one_lt`, `tendsto_pow_const_mul_const_pow_of_abs_lt_one`, `tendsto_pow_const_mul_const_pow_of_lt_one`, `tendsto_self_mul_const_pow_of_abs_lt_one`, `tendsto_self_mul_const_pow_of_lt_one`, `tendsto_smul_comp_nat_floor_of_tendsto_mul`, `tendsto_smul_comp_nat_floor_of_tendsto_nsmul`, `tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder`, `tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded`, `tsum_choose_mul_geometric_of_norm_lt_one`, `tsum_choose_mul_geometric_of_norm_lt_one'`, `tsum_coe_mul_geometric_of_norm_lt_one`, `tsum_coe_mul_geometric_of_norm_lt_one'`, `tsum_geometric_le_of_norm_lt_one`, `tsum_geometric_of_abs_lt_one`, `tsum_geometric_of_norm_lt_one`	90
Total	92

AbsoluteValue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_div_one_add_pow_nhds_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `funLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`map_div₀` `monoidWithZeroHomClass` `Field.isDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `map_one` `Filter.Tendsto.div` `IsTopologicalDivisionRing.toContinuousInv₀` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `tendsto_const_nhds` `Filter.Tendsto.const_add` `IsTopologicalSemiring.toContinuousAdd` `tendsto_pow_atTop_nhds_zero_of_lt_one` `AddGroup.existsAddOfLE` `nonneg` `Filter.Tendsto.const_sub` `IsTopologicalAddGroup.to_continuousSub` `LinearOrderedAddCommGroup.toIsTopologicalAddGroup` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `sub_zero` `add_zero` `le_trans` `map_pow` `le_add` `IsStrictOrderedRing.noZeroDivisors` `add_le` `one_ne_zero` `NeZero.one` `one_div_one`
`tendsto_div_one_add_pow_nhds_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `funLike`	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`div_eq_mul_inv` `one_mul` `map_inv₀` `monoidWithZeroHomClass` `Field.isDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `add_comm` `Filter.Tendsto.inv_tendsto_atTop` `Filter.tendsto_atTop_mono` `le_add` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `map_pow` `map_one` `Filter.Tendsto.congr` `sub_eq_add_neg` `Filter.tendsto_atTop_add_right_of_le` `IsOrderedRing.toIsOrderedAddMonoid` `tendsto_pow_atTop_atTop_of_one_lt` `le_rfl`

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternating_series_le_tendsto` 📖	mathematical	`Filter.Tendsto` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `Antitone` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`monotone_nat_of_le_succ` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Finset.sum_range_succ` `pow_succ'` `Even.neg_pow` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `neg_one_mul` `one_mul` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_le_add_right` `Monotone.ge_of_tendsto` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `Filter.tendsto_atTop_mono` `Filter.tendsto_id`
`cauchySeq_alternating_series_of_tendsto_zero` 📖	mathematical	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`CauchySeq` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNeg` `Real.instOne`	—	`Finset.sum_congr` `mul_comm` `cauchySeq_series_mul_of_tendsto_zero_of_bounded` `norm_sum_neg_one_pow_le`
`cauchySeq_series_mul_of_tendsto_zero_of_bounded` 📖	mathematical	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range`	`CauchySeq` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField`	—	`neg_le_neg` `Real.instIsOrderedAddMonoid` `neg_zero` `Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `Finset.sum_congr` `neg_smul` `Finset.sum_neg_distrib` `neg_neg` `CauchySeq.neg` `SeminormedAddCommGroup.to_isUniformAddGroup` `Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded`
`tendsto_alternating_series_of_tendsto_zero` 📖	mathematical	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNeg` `Real.instOne`	—	`cauchySeq_tendsto_of_complete` `Real.instCompleteSpace` `cauchySeq_alternating_series_of_tendsto_zero`
`tendsto_le_alternating_series` 📖	mathematical	`Filter.Tendsto` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `Antitone` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`antitone_nat_of_succ_le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Finset.sum_range_succ` `pow_succ'` `Even.neg_pow` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `neg_one_mul` `neg_neg` `one_mul` `sub_add_eq_add_sub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_le_add_right` `le_of_tendsto` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `Filter.tendsto_atTop_mono` `Filter.tendsto_id`

HasSummableGeomSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SummationFilter.unconditional`	—	—

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternating_series_le_tendsto` 📖	mathematical	`Filter.Tendsto` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `Monotone` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`monotone_nat_of_le_succ` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Finset.sum_range_succ` `pow_succ'` `Even.neg_pow` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `neg_one_mul` `neg_neg` `one_mul` `sub_add_eq_add_sub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_le_add_right` `ge_of_tendsto` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `Filter.tendsto_atTop_mono` `Filter.tendsto_id`
`cauchySeq_alternating_series_of_tendsto_zero` 📖	mathematical	`Monotone` `Real` `Nat.instPreorder` `Real.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`CauchySeq` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNeg` `Real.instOne`	—	`Finset.sum_congr` `mul_comm` `cauchySeq_series_mul_of_tendsto_zero_of_bounded` `norm_sum_neg_one_pow_le`
`cauchySeq_series_mul_of_tendsto_zero_of_bounded` 📖	mathematical	`Monotone` `Real` `Nat.instPreorder` `Real.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range`	`CauchySeq` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField`	—	`cauchySeq_shift` `Finset.sum_range_by_parts` `Finset.sum_congr` `sub_eq_add_neg` `tsub_zero` `Nat.instOrderedSub` `CauchySeq.add` `SeminormedAddCommGroup.to_isUniformAddGroup` `Filter.Tendsto.cauchySeq` `NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded` `NormedSpace.toIsBoundedSMul` `Filter.eventually_map` `Filter.Eventually.of_forall` `CauchySeq.neg` `cauchySeq_range_of_norm_bounded` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `UniformContinuous.comp_cauchySeq` `Real.uniformContinuous_const_mul` `Finset.sum_range_sub` `CauchySeq.add_const` `instIsUniformAddGroupReal` `norm_smul` `NormedSpace.toNormSMulClass` `mul_comm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `abs_nonneg`
`tendsto_alternating_series_of_tendsto_zero` 📖	mathematical	`Monotone` `Real` `Nat.instPreorder` `Real.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNeg` `Real.instOne`	—	`cauchySeq_tendsto_of_complete` `Real.instCompleteSpace` `cauchySeq_alternating_series_of_tendsto_zero`
`tendsto_le_alternating_series` 📖	mathematical	`Filter.Tendsto` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `Monotone` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`antitone_nat_of_succ_le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Finset.sum_range_succ` `pow_succ'` `Even.neg_pow` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `neg_one_mul` `one_mul` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_le_add_right` `Antitone.le_of_tendsto` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `Filter.tendsto_atTop_mono` `Filter.tendsto_id`

NormedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_series_of_le_geometric'` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Nat.instPreorder` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range`	—	`CauchySeq.comp_tendsto` `cauchy_series_of_le_geometric` `Filter.tendsto_add_atTop_nat`
`cauchy_series_of_le_geometric''` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Nat.instPreorder` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range`	—	`mul_nonneg_iff_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `LE.le.trans` `norm_nonneg` `le_refl` `not_lt` `cauchySeq_sum_of_eventually_eq` `cauchy_series_of_le_geometric'` `norm_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `LT.lt.le`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_pow_div_factorial` 📖	mathematical	—	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`instIsStrictOrderedRing` `LT.lt.trans_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.one` `instNontrivial` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instIsOrderedRing` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.lt_floor_add_one` `pow_succ'` `Nat.factorial_succ` `Nat.cast_mul` `div_mul_div_comm` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_div` `norm_natCast` `Nat.cast_succ` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `div_le_div₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_nonneg` `le_refl` `Right.add_pos_of_nonneg_of_pos` `Nat.cast_nonneg'` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `add_le_add_left` `Nat.mono_cast` `summable_of_ratio_norm_eventually_le` `instCompleteSpace` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`

SeminormedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq_of_le_geometric` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Norm.norm` `toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `toSeminormedAddGroup` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `toPseudoMetricSpace` `Nat.instPreorder`	—	`cauchySeq_of_le_geometric` `dist_eq_norm`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_alternating_series_tsum` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`Filter.Tendsto` `Finset.sum` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `tsum`	—	`tendsto_sum_tsum_nat` `alternating`

Units

Definitions

Name	Category	Theorems
`oneSub` 📖	CompOp	2 math math: `NormedRing.inverse_one_sub`, `val_oneSub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`val_oneSub` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `oneSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—

(root)

Definitions

Name	Category	Theorems
`HasSummableGeomSeries` 📖	CompData	2 math math: `instHasSummableGeomSeriesOfCompleteSpace`, `instHasSummableGeomSeries`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`TFAE_exists_lt_isLittleO_pow` 📖	mathematical	—	`List.TFAE` `Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instNeg` `Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Monoid.toNatPow` `Real.instMonoid` `Real.instZero` `Asymptotics.IsBigO` `Real.instLT` `Filter.Eventually` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup`	—	`LT.lt.trans_le` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans_lt` `Set.Subset.trans` `Set.Ioo_subset_Ico_self` `Asymptotics.IsLittleO.isBigO` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `abs_lt` `covariant_swap_add_of_covariant_add` `abs_nonneg` `Asymptotics.IsBigO.trans_isLittleO` `isLittleO_pow_pow_of_abs_lt_left` `le_abs_self` `Asymptotics.bound_of_isBigO_nat_atTop` `abs_pow` `Real.instIsOrderedRing` `abs_of_nonneg` `LT.lt.le` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `LT.lt.ne'` `sign_cases_of_C_mul_pow_nonneg` `LE.le.trans` `Asymptotics.isBigO_zero` `MulZeroClass.zero_mul` `Asymptotics.isBigO_of_le'` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Filter.Eventually.mono` `Asymptotics.IsLittleO.def` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `abs_of_pos` `one_mul` `Real.norm_eq_abs` `Filter.nonneg_of_eventually_pow_nonneg` `Asymptotics.IsBigO.of_norm_eventuallyLE` `List.tfae_of_cycle`
`alternating_series_error_bound` 📖	mathematical	`Antitone` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`Preorder.toLE` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `tsum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `Finset.range`	—	`Antitone.alternating_series_le_tendsto` `Summable.tendsto_alternating_series_tsum` `Antitone.tendsto_le_alternating_series` `le_of_tendsto` `instClosedIicTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Summable.tendsto_atTop_zero` `IsUniformAddGroup.to_topologicalAddGroup` `Filter.mp_mem` `Filter.Ici_mem_atTop` `Filter.univ_mem'` `Nat.even_or_odd` `Nat.instAtLeastTwoHAddOfNat` `even_iff_exists_two_mul` `abs_sub_le_iff` `IsOrderedRing.toIsOrderedAddMonoid` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `add_comm` `Finset.sum_range_succ` `Even.neg_pow` `Distrib.rightDistribClass` `one_pow` `one_mul` `LE.le.trans` `le_add_of_nonneg_right` `odd_iff_exists_bit1` `Finset.sum_congr` `AddGroup.toOrderedSub` `pow_add` `pow_one` `mul_one` `neg_mul`
`cauchySeq_finset_of_geometric_bound` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `Finset` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `PartialOrder.toPreorder` `Finset.partialOrder` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`cauchySeq_finset_of_norm_bounded` `HasSum.summable` `aux_hasSum_of_le_geometric` `dist_partial_sum_le_of_le_geometric`
`cauchy_series_of_le_geometric` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Nat.instPreorder` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range`	—	`cauchySeq_of_le_geometric` `dist_partial_sum'`
`dist_partial_sum` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`Finset.sum_range_succ` `dist_eq_norm` `add_sub_cancel_left`
`dist_partial_sum'` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`Finset.sum_range_succ` `dist_eq_norm'` `add_sub_cancel_left`
`dist_partial_sum_le_of_le_geometric` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range`	—	`Finset.sum_range_succ` `dist_eq_norm` `norm_neg` `neg_sub` `add_sub_cancel_left`
`exists_norm_le_of_cauchySeq` 📖	mathematical	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Nat.instPreorder` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.range`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`cauchySeq_iff_le_tendsto_0` `dist_partial_sum'` `zero_le` `Nat.instCanonicallyOrderedAdd`
`geom_series_eq_inverse` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SummationFilter.unconditional` `Ring.inverse` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Ring.inverse_unit`
`geom_series_mul_neg` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Summable.tsum_pow_mul_one_sub` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable_geometric_of_norm_lt_one`
`geom_series_mul_one_add` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `add_mul` `Distrib.rightDistribClass` `one_mul` `geom_series_mul_shift` `geom_series_succ` `two_mul` `add_sub_assoc`
`geom_series_mul_shift` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	—	`Summable.tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `summable_geometric_of_norm_lt_one`
`geom_series_succ` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SummationFilter.unconditional` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`eq_sub_iff_add_eq` `Summable.tsum_eq_zero_add` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable_geometric_of_norm_lt_one` `pow_zero` `add_comm`
`hasSum_choose_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.choose` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `AddMonoidWithOne.toOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional`	—	`one_div` `Ring.inverse_eq_inv'` `inv_pow` `hasSum_choose_mul_geometric_of_norm_lt_one'` `instHasSummableGeomSeries`
`hasSum_choose_mul_geometric_of_norm_lt_one'` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.choose` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Ring.inverse` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `SummationFilter.unconditional`	—	`add_zero` `Nat.choose_zero_right` `Nat.cast_one` `one_mul` `zero_add` `pow_one` `hasSum_geom_series_inverse` `summable_norm_mul_geometric_of_norm_lt_one` `Asymptotics.isBigO_iff` `Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.univ_mem'` `Nat.abs_cast` `Real.instIsOrderedRing` `Nat.cast_pow` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Nat.choose_le_choose` `Nat.choose_le_pow` `Finset.sum_congr` `mul_assoc` `pow_add` `Nat.sum_range_add_choose` `add_assoc` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `pow_succ` `hasSum_sum_range_mul_of_summable_norm'` `HasSum.summable` `summable_norm_geometric_of_norm_lt_one` `summable_geometric_of_norm_lt_one`
`hasSum_coe_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `SummationFilter.unconditional`	—	`div_eq_mul_inv` `Ring.inverse_eq_inv'` `inv_pow` `hasSum_coe_mul_geometric_of_norm_lt_one'` `instHasSummableGeomSeries`
`hasSum_coe_mul_geometric_of_norm_lt_one'` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Ring.inverse` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `SummationFilter.unconditional`	—	`Nat.choose_one_right` `Nat.cast_add` `Nat.cast_one` `hasSum_choose_mul_geometric_of_norm_lt_one'` `hasSum_geom_series_inverse` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_sub_cancel_right` `Ring.mul_inverse_cancel` `isUnit_one_sub_of_norm_lt_one` `sub_eq_add_neg` `pow_succ` `pow_zero` `neg_mul` `mul_assoc` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `HasSum.sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`hasSum_geom_series_inverse` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Ring.inverse` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SummationFilter.unconditional`	—	`geom_series_eq_inverse` `Summable.hasSum` `summable_geometric_of_norm_lt_one`
`hasSum_geometric_of_abs_lt_one` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	`HasSum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `Real.instSub` `SummationFilter.unconditional`	—	`hasSum_geometric_of_norm_lt_one`
`hasSum_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `SummationFilter.unconditional`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendsto_pow_atTop_nhds_zero_of_norm_lt_one` `tendsto_const_nhds` `hasSum_iff_tendsto_nat_of_summable_norm` `norm_pow` `NormedDivisionRing.toNormMulClass` `summable_geometric_of_lt_one` `norm_nonneg` `geom_sum_eq` `div_eq_mul_inv` `zero_sub` `neg_mul` `one_mul` `neg_inv` `neg_sub`
`instHasSummableGeomSeries` 📖	mathematical	—	`HasSummableGeomSeries` `NormedDivisionRing.toNormedRing`	—	`HasSum.summable` `hasSum_geometric_of_norm_lt_one`
`instHasSummableGeomSeriesOfCompleteSpace` 📖	mathematical	—	`HasSummableGeomSeries`	—	`summable_geometric_of_lt_one` `norm_nonneg` `Summable.of_norm_bounded_eventually_nat` `eventually_norm_pow_le`
`isBigO_pow_pow_of_le_left` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Monoid.toNatPow` `Real.instMonoid`	—	`LE.le.eq_or_lt` `Asymptotics.isBigO_refl` `Asymptotics.IsLittleO.isBigO` `isLittleO_pow_pow_of_lt_left`
`isLittleO_coe_const_pow_of_one_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Asymptotics.IsLittleO` `NormedRing.toNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Monoid.toNatPow` `Real.instMonoid`	—	`pow_one` `isLittleO_pow_const_const_pow_of_one_lt`
`isLittleO_pow_const_const_pow_of_one_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Asymptotics.IsLittleO` `NormedRing.toNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instMonoid`	—	`Filter.Tendsto.mono_left` `Continuous.tendsto'` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id` `one_pow` `inf_le_left` `Filter.Eventually.exists` `nhdsGT_neBot` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.Eventually.and` `Filter.Tendsto.eventually` `gt_mem_nhds` `self_mem_nhdsWithin` `LE.le.trans` `zero_le_one` `Real.instZeroLEOneClass` `LT.lt.le` `pow_mul` `mul_comm` `mul_right_comm` `Nat.norm_cast_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_eq_inv_mul` `Nat.cast_le_pow_div_sub` `norm_nonneg` `Asymptotics.IsBigO.pow` `Asymptotics.isBigO_of_le'` `Asymptotics.IsBigO.trans_isLittleO` `isLittleO_pow_pow_of_lt_left` `pow_nonneg` `IsOrderedRing.toPosMulMono`
`isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instMonoid`	—	`Asymptotics.IsLittleO.congr'` `Asymptotics.isLittleO_zero` `Filter.mem_atTop_sets` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `zero_pow` `MulZeroClass.mul_zero` `Filter.EventuallyEq.rfl` `isLittleO_pow_const_const_pow_of_one_lt` `one_lt_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `Asymptotics.IsBigO.of_norm_eventuallyLE` `eventually_norm_pow_le` `div_pow` `div_mul_cancel₀` `LT.lt.ne'` `pow_pos` `Real.instZeroLEOneClass` `Asymptotics.IsLittleO.mul_isBigO` `NormedDivisionRing.toNormMulClass`
`isLittleO_pow_pow_of_abs_lt_left` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Monoid.toNatPow` `Real.instMonoid`	—	`Asymptotics.IsLittleO.of_norm_right` `Asymptotics.IsLittleO.of_norm_left` `Asymptotics.IsLittleO.congr` `isLittleO_pow_pow_of_lt_left` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `pow_abs` `Real.instIsOrderedRing`
`isLittleO_pow_pow_of_lt_left` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Monoid.toNatPow` `Real.instMonoid`	—	`LE.le.trans_lt` `Asymptotics.isLittleO_of_tendsto` `LT.lt.ne'` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Filter.Tendsto.congr` `div_pow` `tendsto_pow_atTop_nhds_zero_of_lt_one` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LE.le.trans` `LT.lt.le` `div_lt_one`
`isUnit_one_sub_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`mul_neg_geom_series` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	—	`Summable.one_sub_mul_tsum_pow` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable_geometric_of_norm_lt_one`
`norm_sub_le_of_geometric_bound_of_hasSum` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `HasSum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Finset.sum` `Finset.range` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub`	—	`dist_eq_norm` `dist_le_of_le_geometric_of_tendsto` `dist_partial_sum_le_of_le_geometric` `HasSum.tendsto_sum_nat`
`norm_sum_neg_one_pow_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Real.norm` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `Real.instMonoid` `Real.instNeg` `Real.instOne`	—	`neg_one_geom_sum` `norm_zero` `Real.instZeroLEOneClass` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass`
`not_summable_of_ratio_norm_eventually_ge` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Filter.Frequently` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instZero` `Filter.atTop` `Nat.instPreorder` `Filter.Eventually` `Real.instLE` `Real.instMul`	`Summable` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.frequently_atTop` `summable_nat_add_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Summable.tendsto_atTop_zero` `not_tendsto_atTop_of_tendsto_nhds` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.atTop_neBot` `Filter.Tendsto.comp` `tendsto_norm_zero` `tendsto_atTop_of_geom_le` `lt_of_le_of_ne` `norm_nonneg` `zero_add`
`not_summable_of_ratio_test_tendsto_gt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Filter.Tendsto` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Summable` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`Filter.mp_mem` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.univ_mem'` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `div_zero` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `not_summable_of_ratio_norm_eventually_ge` `Filter.Eventually.frequently` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `lt_of_le_of_ne` `norm_nonneg`
`summable_choose_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.choose` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	—	`HasSum.summable` `hasSum_choose_mul_geometric_of_norm_lt_one'`
`summable_descFactorial_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.descFactorial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	—	`Nat.descFactorial_eq_factorial_mul_choose` `Nat.cast_mul` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `summable_choose_mul_geometric_of_norm_lt_one`
`summable_geometric_iff_norm_lt_one` 📖	mathematical	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SummationFilter.unconditional` `Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	—	`Filter.Eventually.exists` `Filter.cofinite_neBot` `instInfiniteNat` `Filter.Tendsto.eventually` `Summable.tendsto_cofinite_zero` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Metric.ball_mem_nhds` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `lt_of_pow_lt_pow_left₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `zero_le_one` `one_pow` `dist_zero_right` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `summable_geometric_of_norm_lt_one` `instHasSummableGeomSeries`
`summable_geometric_of_abs_lt_one` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional`	—	`summable_geometric_of_norm_lt_one` `instHasSummableGeomSeries`
`summable_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SummationFilter.unconditional`	—	`HasSummableGeomSeries.summable_geometric_of_norm_lt_one`
`summable_norm_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SummationFilter.unconditional`	—	`pow_zero` `one_mul` `summable_norm_pow_mul_geometric_of_norm_lt_one`
`summable_norm_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne` `Asymptotics.IsBigO` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instNatCast` `Monoid.toNatPow` `Nat.instMonoid`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	—	`exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `summable_of_isBigO_nat` `Real.instCompleteSpace` `summable_geometric_of_lt_one` `LE.le.trans` `norm_nonneg` `LT.lt.le` `norm_norm` `Asymptotics.IsBigOWith.isBigO` `Asymptotics.IsBigOWith.of_bound` `Filter.mp_mem` `eventually_norm_pow_le` `Filter.univ_mem'` `abs_norm` `norm_mul` `NormedDivisionRing.toNormMulClass` `Nat.abs_cast` `Real.instIsOrderedRing` `norm_pow` `NormedDivisionRing.to_normOneClass` `norm_mul_le` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Nat.norm_cast_le` `mul_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `le_of_eq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Asymptotics.IsBigO.mul` `Asymptotics.isBigO_refl` `Nat.cast_pow` `Asymptotics.IsLittleO.isBigO` `isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt`
`summable_norm_pow_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SummationFilter.unconditional`	—	`summable_norm_mul_geometric_of_norm_lt_one` `Asymptotics.isBigO_refl`
`summable_of_ratio_norm_eventually_le` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Filter.Eventually` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `Filter.atTop` `Nat.instPreorder`	`Summable` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SummationFilter.unconditional`	—	`Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `summable_nat_add_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Summable.of_norm_bounded` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_geometric_of_lt_one` `mul_comm` `zero_add` `le_geom` `Summable.of_norm_bounded_eventually_nat` `summable_zero` `Filter.mp_mem` `Filter.univ_mem'` `not_lt` `norm_nonneg` `lt_of_le_of_lt` `mul_neg_of_neg_of_pos` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing`
`summable_of_ratio_test_tendsto_lt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Filter.atTop` `Nat.instPreorder` `Filter.Tendsto` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `summable_of_ratio_norm_eventually_le` `Filter.mp_mem` `Filter.Tendsto.eventually_le_const` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.univ_mem'` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_pos_iff`
`summable_pow_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SummationFilter.unconditional`	—	`Nat.strong_induction_on` `Polynomial.Monic.comp_X_add_C` `monic_ascPochhammer` `Nat.instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Polynomial.natDegree_comp` `ascPochhammer_natDegree` `Polynomial.natDegree_X_add_C` `mul_one` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Polynomial.eval_comp` `Polynomial.eval_add` `Polynomial.eval_X` `Polynomial.eval_one` `ascPochhammer_nat_eq_descFactorial` `Polynomial.Monic.as_sum` `Finset.sum_congr` `Polynomial.eval_pow` `Polynomial.eval_finset_sum` `Polynomial.eval_mul` `Polynomial.eval_natCast` `Summable.sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `summable_descFactorial_mul_geometric_of_norm_lt_one` `summable_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `mul_assoc` `Summable.mul_left` `Nat.cast_add` `Nat.cast_pow` `Nat.cast_sum` `Nat.cast_mul` `add_mul` `Distrib.rightDistribClass` `Finset.sum_mul` `add_sub_cancel_right`
`summable_powerSeries_of_norm_lt` 📖	mathematical	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Nat.instPreorder` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm`	`Summable` `SummationFilter.unconditional`	—	`LE.le.trans_lt` `norm_nonneg` `exists_norm_le_of_cauchySeq` `summable_iff_cauchySeq_finset` `cauchySeq_finset_of_geometric_bound` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `div_pow` `mul_comm_div` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono`
`summable_powerSeries_of_norm_lt_one` 📖	mathematical	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Nat.instPreorder` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Finset.range` `Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`Summable` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SummationFilter.unconditional`	—	`summable_powerSeries_of_norm_lt` `Finset.sum_congr` `one_pow` `mul_one` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass`
`tendsto_const_div_pow` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`Nat.cast_pow` `Filter.Tendsto.const_div_atTop` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Filter.Tendsto.comp` `tendsto_natCast_atTop_atTop` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.tendsto_pow_atTop` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing`
`tendsto_intCast_atBot_cobounded` 📖	mathematical	—	`Filter.Tendsto` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Filter.atBot` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`Filter.Tendsto.mono_left` `tendsto_intCast_atBot_sup_atTop_cobounded` `le_sup_left`
`tendsto_intCast_atBot_sup_atTop_cobounded` 📖	mathematical	—	`Filter.Tendsto` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Filter` `Filter.instSup` `Filter.atBot` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Filter.atTop` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`tendsto_norm_atTop_iff_cobounded` `norm_intCast_eq_abs_mul_norm_one` `Int.cast_abs` `Real.instIsStrictOrderedRing` `Filter.Tendsto.atTop_mul_const` `norm_pos_iff` `one_ne_zero` `NeZero.one` `Filter.Tendsto.comp` `tendsto_intCast_atTop_atTop` `Real.instArchimedean` `Filter.Tendsto.sup` `Filter.tendsto_abs_atBot_atTop` `Int.instIsOrderedAddMonoid` `Filter.tendsto_abs_atTop_atTop`
`tendsto_intCast_atTop_cobounded` 📖	mathematical	—	`Filter.Tendsto` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`Filter.Tendsto.mono_left` `tendsto_intCast_atBot_sup_atTop_cobounded` `le_sup_right`
`tendsto_natCast_atTop_cobounded` 📖	mathematical	—	`Filter.Tendsto` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`tendsto_norm_atTop_iff_cobounded` `norm_natCast_eq_mul_norm_one` `Filter.Tendsto.atTop_mul_const` `Real.instIsStrictOrderedRing` `norm_pos_iff` `one_ne_zero` `NeZero.one` `tendsto_natCast_atTop_atTop` `Real.instIsOrderedRing` `Real.instArchimedean`
`tendsto_pow_atTop_nhds_zero_iff_norm_lt_one` 📖	mathematical	—	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Real` `Real.instLT` `Norm.norm` `SeminormedRing.toNorm` `Real.instOne`	—	`abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_nonneg` `tendsto_pow_atTop_nhds_zero_iff` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `instOrderTopologyReal` `tendsto_zero_iff_norm_tendsto_zero` `Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `Nat.le_induction` `pow_one` `pow_succ` `norm_mul` `tendsto_pow_atTop_nhds_zero_of_norm_lt_one`
`tendsto_pow_atTop_nhds_zero_of_abs_lt_one` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	`Filter.Tendsto` `Monoid.toNatPow` `Real.instMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`tendsto_pow_atTop_nhds_zero_of_norm_lt_one`
`tendsto_pow_atTop_nhds_zero_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `SeminormedRing.toNorm` `Real.instOne`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`squeeze_zero_norm'` `eventually_norm_pow_le` `tendsto_pow_atTop_nhds_zero_of_lt_one` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `norm_nonneg`
`tendsto_pow_const_div_const_pow_of_one_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Filter.Tendsto` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`Asymptotics.IsLittleO.tendsto_div_nhds_zero` `isLittleO_pow_const_const_pow_of_one_lt`
`tendsto_pow_const_mul_const_pow_of_abs_lt_one` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	`Filter.Tendsto` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`Filter.Tendsto.congr'` `Filter.mem_atTop_sets` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `isReduced_of_noZeroDivisors` `Real.instNontrivial` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `Nat.instZeroLEOneClass` `tendsto_const_nhds` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `tendsto_zero_iff_norm_tendsto_zero` `norm_mul` `norm_pow` `NormedDivisionRing.to_normOneClass` `Nat.abs_cast` `Real.instIsOrderedRing` `inv_pow` `div_eq_mul_inv` `inv_inv` `tendsto_pow_const_div_const_pow_of_one_lt`
`tendsto_pow_const_mul_const_pow_of_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`Filter.Tendsto` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`tendsto_pow_const_mul_const_pow_of_abs_lt_one` `abs_lt` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.trans_le` `neg_one_lt_zero` `Real.instZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`tendsto_self_mul_const_pow_of_abs_lt_one` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	`Filter.Tendsto` `Real.instMul` `Real.instNatCast` `Monoid.toNatPow` `Real.instMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`pow_one` `tendsto_pow_const_mul_const_pow_of_abs_lt_one`
`tendsto_self_mul_const_pow_of_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`Filter.Tendsto` `Real.instMul` `Real.instNatCast` `Monoid.toNatPow` `Real.instMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`pow_one` `tendsto_pow_const_mul_const_pow_of_lt_one`
`tendsto_smul_comp_nat_floor_of_tendsto_mul` 📖	mathematical	`Filter.Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Nat.floor` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `PartialOrder.toPreorder`	—	`tendsto_smul_comp_nat_floor_of_tendsto_nsmul` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE` `nsmul_eq_mul`
`tendsto_smul_comp_nat_floor_of_tendsto_nsmul` 📖	mathematical	`Filter.Tendsto` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Nat.floor` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `PartialOrder.toPreorder`	—	`Nat.cast_smul_eq_nsmul` `tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder` `Filter.Tendsto.comp` `tendsto_nat_floor_atTop` `tendsto_natCast_atTop_cobounded` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Filter.isBoundedUnder_of_eventually_le` `Filter.Eventually.mono` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `SemilatticeSup.instIsDirectedOrder` `Nontrivial.to_nonempty` `Nat.cast_one` `Nat.abs_floor_sub_le` `norm_le_norm_of_abs_le_abs`
`tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder` 📖	—	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `nhds` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing`	—	—	`Filter.Tendsto.congr_dist` `dist_eq_norm` `norm_smul` `Filter.isBoundedUnder_le_mul_tendsto_zero` `norm_norm` `tendsto_zero_iff_norm_tendsto_zero` `tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded` `Filter.Tendsto.isBoundedUnder_le` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.Tendsto.norm`
`tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded` 📖	mathematical	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Filter.Tendsto` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	`nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Filter.IsBoundedUnder.eventually_le` `Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_closedBall` `Filter.mp_mem` `Filter.Tendsto.eventually_ne_cobounded` `Filter.hasBasis_cobounded_norm` `Filter.univ_mem'` `eq_or_lt_of_le` `LE.le.trans` `norm_nonneg` `smul_eq_zero_iff_right` `IsDomain.toIsCancelMulZero` `norm_le_zero_iff` `dist_self` `LT.lt.le` `dist_zero_right` `le_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `norm_smul` `div_le_div₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `le_refl` `div_pos` `div_div_cancel₀` `LT.lt.ne'`
`tsum_choose_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.choose` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SummationFilter.unconditional` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `AddMonoidWithOne.toOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_choose_mul_geometric_of_norm_lt_one`
`tsum_choose_mul_geometric_of_norm_lt_one'` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.choose` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional` `Ring.inverse` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_choose_mul_geometric_of_norm_lt_one'`
`tsum_coe_mul_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SummationFilter.unconditional` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_coe_mul_geometric_of_norm_lt_one`
`tsum_coe_mul_geometric_of_norm_lt_one'` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SummationFilter.unconditional` `Ring.inverse` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_coe_mul_geometric_of_norm_lt_one'` `instHasSummableGeomSeries`
`tsum_geometric_le_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Real.instLE` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SummationFilter.unconditional` `Real.instAdd` `Real.instSub` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instInv`	—	`Summable.tsum_eq_zero_add` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `pow_zero` `le_trans` `norm_add_le` `tsum_of_norm_bounded` `Finset.sum_singleton` `hasSum_nat_add_iff'` `instIsTopologicalAddGroupReal` `hasSum_geometric_of_lt_one` `norm_nonneg` `norm_pow_le'` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `CancelDenoms.add_subst` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `tsum_eq_zero_of_not_summable` `norm_zero` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `norm_of_subsingleton` `zero_sub` `sub_zero` `inv_one` `neg_add_cancel` `one_le_norm_one` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.add_nonpos`
`tsum_geometric_of_abs_lt_one` 📖	mathematical	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instOne`	`tsum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional` `Real.instInv` `Real.instSub`	—	`tsum_geometric_of_norm_lt_one`
`tsum_geometric_of_norm_lt_one` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instOne`	`tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SummationFilter.unconditional` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_geometric_of_norm_lt_one`

---

← Back to Index