Documentation Verification Report

AbelLimit

📁 Source: Mathlib/Analysis/Complex/AbelLimit.lean

Statistics

Metric	Count
Definitions `stolzCone`, `stolzSet`	2
Theorems `abel_aux`, `nhdsWithin_lt_le_nhdsWithin_stolzSet`, `nhdsWithin_stolzCone_le_nhdsWithin_stolzSet`, `stolzCone_subset_stolzSet_aux`, `stolzSet_empty`, `tendsto_tsum_powerSeries_nhdsWithin_lt`, `tendsto_tsum_powerSeries_nhdsWithin_stolzCone`, `tendsto_tsum_powerSeries_nhdsWithin_stolzSet`, `tendsto_tsum_powerSeries_nhdsWithin_lt`	9
Total	11

Complex

Definitions

Name	Category	Theorems
`stolzCone` 📖	CompOp	3 math math: `tendsto_tsum_powerSeries_nhdsWithin_stolzCone`, `stolzCone_subset_stolzSet_aux`, `nhdsWithin_stolzCone_le_nhdsWithin_stolzSet`
`stolzSet` 📖	CompOp	5 math math: `nhdsWithin_lt_le_nhdsWithin_stolzSet`, `stolzCone_subset_stolzSet_aux`, `nhdsWithin_stolzCone_le_nhdsWithin_stolzSet`, `tendsto_tsum_powerSeries_nhdsWithin_stolzSet`, `stolzSet_empty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abel_aux` 📖	mathematical	`Filter.Tendsto` `Complex` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds` `Real` `Real.instLT` `Norm.norm` `instNorm` `Real.instOne`	`instMul` `instSub` `instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `tsum` `SummationFilter.unconditional`	—	`Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasSum.tendsto_sum_nat` `Summable.hasSum` `summable_powerSeries_of_norm_lt_one` `instCompleteSpace` `Filter.Tendsto.cauchySeq` `MulZeroClass.zero_mul` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `neg_sub` `neg_zero` `Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `tendsto_sub_nhds_zero_iff` `geom_sum_eq` `Mathlib.Tactic.Contrapose.contrapose₃` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `sub_div` `sub_eq_add_neg` `neg_div` `zero_add` `zero_div` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `Filter.Tendsto.div_const` `tendsto_pow_atTop_nhds_zero_of_norm_lt_one` `T2Space.t1Space` `instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.const_mul` `Finset.mul_sum` `Finset.sum_congr` `Finset.sum_Ico_eq_sub` `Finset.mem_range` `Finset.range_eq_Ico` `mul_comm` `MulZeroClass.mul_zero` `mul_add` `Distrib.leftDistribClass` `Finset.sum_add_distrib` `add_mul` `Distrib.rightDistribClass` `sub_add_sub_cancel`
`nhdsWithin_lt_le_nhdsWithin_stolzSet` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Filter` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.map` `ofReal` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.Iio` `Real.instPreorder` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instOne` `stolzSet`	—	`Filter.tendsto_id'` `Filter.tendsto_map'` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `tendsto_nhdsWithin_of_tendsto_nhds` `Continuous.tendsto'` `ContinuousLinearMap.continuous` `Nat.instAtLeastTwoHAddOfNat` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `norm_real` `Real.norm_of_nonneg` `LT.lt.le` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `lt_mul_left` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing`
`nhdsWithin_stolzCone_le_nhdsWithin_stolzSet` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instOne` `stolzCone` `stolzSet`	—	`stolzCone_subset_stolzSet_aux` `nhdsWithin_le_iff` `mem_nhdsWithin` `isOpen_lt` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `continuous_const` `continuous_re` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono`
`stolzCone_subset_stolzSet_aux` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Complex` `Set.instHasSubset` `Set.instInter` `setOf` `Real.instSub` `Real.instOne` `re` `stolzCone` `stolzSet`	—	`mul_pos_iff_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LE.le.trans_lt` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `sub_re` `one_re` `Set.mem_setOf_eq` `stolzCone.eq_1` `sub_lt_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `zero_sub` `neg_sq` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `norm_nonneg` `norm_eq_sqrt_sq_add_sq` `sub_sub_cancel`
`stolzSet_empty` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`stolzSet` `Set` `Complex` `Set.instEmptyCollection`	—	`Set.ext` `stolzSet.eq_1` `Set.mem_setOf` `Set.mem_empty_iff_false` `not_lt` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `LT.lt.le` `one_mul` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `norm_sub_norm_le`
`tendsto_tsum_powerSeries_nhdsWithin_lt` 📖	mathematical	`Filter.Tendsto` `Complex` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds`	`tsum` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `SummationFilter.unconditional` `Filter.map` `Real` `ofReal` `nhdsWithin` `Real.pseudoMetricSpace` `Real.instOne` `Set.Iio` `Real.instPreorder`	—	`Filter.Tendsto.mono_left` `Nat.instAtLeastTwoHAddOfNat` `tendsto_tsum_powerSeries_nhdsWithin_stolzSet` `nhdsWithin_lt_le_nhdsWithin_stolzSet` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`tendsto_tsum_powerSeries_nhdsWithin_stolzCone` 📖	mathematical	`Filter.Tendsto` `Complex` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds` `Real` `Real.instLT` `Real.instZero`	`tsum` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `SummationFilter.unconditional` `nhdsWithin` `instOne` `stolzCone`	—	`Filter.Tendsto.mono_left` `nhdsWithin_stolzCone_le_nhdsWithin_stolzSet` `tendsto_tsum_powerSeries_nhdsWithin_stolzSet`
`tendsto_tsum_powerSeries_nhdsWithin_stolzSet` 📖	mathematical	`Filter.Tendsto` `Complex` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds`	`tsum` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `SummationFilter.unconditional` `nhdsWithin` `instOne` `stolzSet`	—	`le_or_gt` `stolzSet_empty` `nhdsWithin_empty` `Metric.tendsto_atTop` `Metric.tendsto_nhdsWithin_nhds` `dist_eq_norm` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `lt_trans` `Nat.cast_one` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.sum_nonneg` `norm_nonneg` `abel_aux` `norm_sub_rev` `mul_add` `Distrib.leftDistribClass` `Finset.sum_range_add_sum_Ico` `le_max_left` `norm_add_le` `norm_mul` `NormedDivisionRing.toNormMulClass` `add_le_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Finset.sum_congr` `NormedDivisionRing.to_normOneClass` `Finset.sum_le_sum` `mul_one` `pow_le_one₀` `LT.lt.le` `le_of_not_gt` `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.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.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `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.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `Int.instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Int.instCharZero` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_add` `Finset.mem_Ico` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Finset.mul_sum` `mul_assoc` `Summable.sum_le_tsum` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `summable_geometric_of_lt_one` `mul_nonneg` `le_of_lt` `tsum_geometric_of_lt_one` `div_eq_mul_inv` `div_lt_div_of_pos_right` `mul_lt_mul_of_pos_right` `lt_of_not_ge` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `mul_rotate` `mul_div_cancel_right₀` `GroupWithZero.toMulDivCancelClass` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `div_mul_cancel₀` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_overlap_pf` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_mul` `CancelDenoms.add_subst` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `sub_add_cancel` `add_halves` `CharZero.NeZero.two`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_tsum_powerSeries_nhdsWithin_lt` 📖	mathematical	`Filter.Tendsto` `Real` `Finset.sum` `instAddCommMonoid` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace`	`tsum` `instMul` `Monoid.toNatPow` `instMonoid` `SummationFilter.unconditional` `nhdsWithin` `instOne` `Set.Iio` `instPreorder`	—	`Continuous.tendsto` `ContinuousLinearMap.continuous` `Filter.Tendsto.mono_right` `Filter.Tendsto.comp` `Filter.tendsto_map` `Complex.tendsto_tsum_powerSeries_nhdsWithin_lt` `Complex.ofReal_sum` `Metric.tendsto_nhdsWithin_nhds` `dist_eq_norm` `Complex.norm_real` `Filter.tendsto_map'_iff`

---

← Back to Index