Documentation Verification Report

Summable

📁 Source: Mathlib/Algebra/Module/ZLattice/Summable.lean

Statistics

Metric	Count
Definitions `normBound`, `tsumNormRPowBound`	2
Theorems `abs_repr_le`, `abs_repr_lt_of_norm_lt`, `exists_finsetSum_norm_rpow_le_tsum`, `exists_forall_abs_repr_le_norm`, `le_norm_of_le_abs_repr`, `normBound_pos`, `normBound_spec`, `sum_piFinset_Icc_rpow_le`, `summable_norm_pow_inv`, `summable_norm_rpow`, `summable_norm_sub_inv_pow`, `summable_norm_sub_rpow`, `summable_norm_sub_zpow`, `summable_norm_zpow`, `tsumNormRPowBound_pos`, `tsumNormRPowBound_spec`, `tsum_norm_rpow_le`	17
Total	19

ZLattice

Definitions

Name	Category	Theorems
`normBound` 📖	CompOp	5 math math: `normBound_pos`, `le_norm_of_le_abs_repr`, `normBound_spec`, `sum_piFinset_Icc_rpow_le`, `abs_repr_le`
`tsumNormRPowBound` 📖	CompOp	3 math math: `tsum_norm_rpow_le`, `tsumNormRPowBound_spec`, `tsumNormRPowBound_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_repr_le` 📖	mathematical	—	`Real` `Real.instLE` `Real.instIntCast` `abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommGroup` `Int.instRing` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Real.instMul` `Real.instInv` `normBound` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup`	—	`RingHomInvPair.ids` `le_inv_mul_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `normBound_pos` `normBound_spec`
`abs_repr_lt_of_norm_lt` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `Int.instRing` `Real.instMul` `normBound` `Real.instNatCast`	`abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommGroup` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr`	—	`RingHomInvPair.ids` `Int.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `LE.le.trans_lt` `abs_repr_le` `inv_mul_lt_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `normBound_pos`
`exists_finsetSum_norm_rpow_le_tsum` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Finset.sum` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Real.instAddCommMonoid` `Real.instPow` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `Int.instRing` `Real.instMul` `tsum` `Real.pseudoMetricSpace` `Real.instNatCast` `Real.instAdd` `Real.instSub` `Module.finrank` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Real.instOne` `SummationFilter.unconditional`	—	`subsingleton_or_nontrivial` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `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_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `neg_eq_zero` `sub_eq_zero_of_eq` `Finset.sum_congr` `norm_zero` `Real.zero_rpow` `Finset.sum_const_zero` `Real.one_rpow` `one_mul` `tsum_nonneg` `Real.instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.rpow_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instModuleFree_of_discrete_submodule` `instModuleFinite_of_discrete_submodule` `Module.finrank_eq_card_basis` `commRing_strongRankCondition` `Int.instNontrivial` `Module.Free.instNonemptyChooseBasisIndexOfNontrivial` `Nat.instAtLeastTwoHAddOfNat` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `Fintype.card_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `normBound_pos` `RingHomInvPair.ids` `RingHomCompTriple.ids` `Finite.of_fintype` `Finset.coe_injective` `Finset.coe_image` `Set.image_congr` `Equiv.image_symm_image` `Finset.sum_image` `EquivLike.toEmbeddingLike` `Bornology.IsBounded.subset_closedBall_lt` `IsCompact.isBounded` `Set.Finite.isCompact` `Finset.finite_toSet` `Mathlib.Meta.Positivity.int_floor_nonneg_of_pos` `Int.instIsOrderedAddMonoid` `dist_zero_right` `pi_norm_le_iff_of_nonneg` `LT.lt.le` `LE.le.trans` `Finset.sum_le_sum_of_subset_of_nonneg` `norm_nonneg` `Submodule.addSubgroupClass` `Module.Basis.repr_symm_apply` `Finsupp.sum_zsmul` `sum_piFinset_Icc_rpow_le` `mul_assoc` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `mul_nonneg` `IsOrderedRing.toPosMulMono` `le_of_lt` `Real.rpow_pos_of_pos` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.mul_rpow` `mul_le_mul_of_nonneg_right` `Real.rpow_neg_one` `Real.rpow_mul` `Real.self_le_rpow_of_one_le` `not_le` `neg_mul` `le_neg` `covariant_swap_add_of_covariant_add`
`exists_forall_abs_repr_le_norm` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instMul` `Real.instIntCast` `abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommGroup` `Int.instRing` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup`	—	`RingHomInvPair.ids` `Module.Finite.finite_basis` `Int.instNontrivial` `instModuleFinite_of_discrete_submodule` `Real.instIsStrictOrderedRing` `instHasSolidNormReal` `FiniteDimensional.proper_real` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `RingHomCompTriple.ids` `Continuous.isOpen_preimage` `ContinuousLinearEquiv.continuous` `isOpen_set_pi` `Set.finite_univ` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `Real.instIsOrderedAddMonoid` `Metric.isOpen_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `abs_zero` `Int.instAddLeftMono` `Int.cast_zero` `MulZeroClass.mul_zero` `norm_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `abs_mul` `abs_inv` `abs_norm` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Module.Basis.ofZLatticeBasis_repr_apply` `covariant_swap_add_of_covariant_add` `dist_zero_right` `norm_smul` `NormedSpace.toNormSMulClass` `norm_div` `abs_eq_self` `LT.lt.le` `Real.norm_ofNat` `norm_inv` `norm_norm` `inv_mul_cancel₀` `mul_one` `Int.cast_abs` `le_of_lt` `inv_mul_lt_iff₀` `norm_pos_iff` `mul_left_comm` `IsScalarTower.left` `comap_discreteTopology` `ContinuousMapClass.map_continuous` `ContinuousSemilinearMapClass.toContinuousMapClass` `LinearMap.continuousLinearMapClassOfFiniteDimensional` `Submodule.topologicalAddGroup` `SMulMemClass.continuousSMul` `Submodule.smulMemClass` `instT2SpaceSubtype` `FiniteDimensional.finiteDimensional_submodule` `Subtype.val_injective` `AddCommGroup.intIsScalarTower` `Submodule.subset_span` `Submodule.map_injective_of_injective` `RingHomSurjective.ids` `Submodule.subtype_injective` `Submodule.map.congr_simp` `Submodule.span_span_coe_preimage` `Submodule.map_top` `Submodule.range_subtype`
`le_norm_of_le_abs_repr` 📖	mathematical	`abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommGroup` `Int.instRing` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr`	`Real` `Real.instLE` `Real.instMul` `normBound` `Real.instNatCast` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup`	—	`RingHomInvPair.ids` `Mathlib.Tactic.Contrapose.contrapose₁` `abs_repr_lt_of_norm_lt`
`normBound_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `normBound`	—	`RingHomInvPair.ids` `exists_forall_abs_repr_le_norm`
`normBound_spec` 📖	mathematical	—	`Real` `Real.instLE` `Real.instMul` `normBound` `Real.instIntCast` `abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommGroup` `Int.instRing` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup`	—	`RingHomInvPair.ids` `exists_forall_abs_repr_le_norm`
`sum_piFinset_Icc_rpow_le` 📖	mathematical	`Fintype.card` `Real` `Real.instLT` `Real.instNeg` `Real.instNatCast`	`Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Fintype.piFinset` `Finset.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Real.instPow` `Norm.norm` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `Int.instRing` `Submodule.addCommMonoid` `Finset.univ` `AddSubgroupClass.zsmul` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Submodule.addSubgroupClass` `DFunLike.coe` `Module.Basis` `Submodule.addCommGroup` `Module.Basis.instFunLike` `Real.instMul` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `normBound` `tsum` `Real.pseudoMetricSpace` `Real.instAdd` `Real.instSub` `Real.instOne` `SummationFilter.unconditional`	—	`Submodule.addSubgroupClass` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.trans_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.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `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_zero_add` `Mathlib.Tactic.Ring.neg_congr` `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.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Fintype.card_eq_zero_iff` `Finset.sum_congr` `Fintype.piFinset_of_isEmpty` `Finset.univ_unique` `Finset.univ_eq_empty` `norm_zero` `Real.zero_rpow` `LT.lt.ne` `Finset.sum_const_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.mul_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `MulZeroClass.zero_mul` `zero_sub` `Finset.ext` `Int.instCharZero` `neg_zero` `Finset.Icc_self` `Fintype.piFinset_singleton` `Finset.card_sdiff_of_subset` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Fintype.card_piFinset` `Finset.prod_congr` `Int.card_Icc` `Finset.prod_const` `normBound_pos` `Submodule.addSubmonoidClass` `AddSubmonoidClass.coe_finset_sum` `Finset.sum_eq_sum_range_sdiff` `Finset.sum_singleton` `zero_smul` `zero_add` `Finset.sum_le_sum` `Real.instIsOrderedAddMonoid` `Nat.cast_one` `Nat.cast_add` `Real.rpow_le_rpow_of_nonpos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `zero_le` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Finset.mem_sdiff` `le_norm_of_le_abs_repr` `Finset.mem_Icc` `abs_le` `Int.instIsOrderedAddMonoid` `RingHomInvPair.ids` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Module.Basis.repr_self` `Finsupp.smul_single` `Finsupp.coe_finset_sum` `Finset.sum_apply` `Finsupp.single_apply` `Finset.sum_ite_eq'` `instNoMaxOrderOfNontrivial` `Int.instIsStrictOrderedRing` `Int.instNontrivial` `mul_comm` `LT.lt.le` `Finset.sum_const` `nsmul_eq_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Nat.mono_cast` `LE.le.trans` `mul_le_mul_right` `Nat.instMulLeftMono` `pow_le_pow_left'` `covariant_swap_mul_of_covariant_mul` `le_of_lt` `Real.rpow_pos_of_pos` `Nat.cast_nonneg'` `Real.instNontrivial` `Finset.mul_sum` `Nat.cast_mul` `Nat.cast_pow` `Real.mul_rpow` `mul_pow` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `add_zero` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Real.rpow_natCast` `Real.rpow_add` `Nat.cast_sub` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Finset.sum_range_succ'` `le_add_iff_nonneg_right` `Real.rpow_nonneg` `lt_of_lt_of_le` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Summable.sum_le_tsum` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `Real.summable_nat_rpow` `lt_of_not_ge` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le`
`summable_norm_pow_inv` 📖	mathematical	`Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `SummationFilter.unconditional`	—	`inv_pow` `sub_zero` `summable_norm_sub_inv_pow`
`summable_norm_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.instNatCast` `Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Summable` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.instPow` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `SummationFilter.unconditional`	—	`summable_of_sum_le` `Real.rpow_nonneg` `norm_nonneg` `tsumNormRPowBound_spec`
`summable_norm_sub_inv_pow` 📖	mathematical	`Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional`	—	`inv_pow` `zpow_neg` `zpow_natCast` `summable_norm_sub_zpow` `neg_lt_neg` `Int.instIsOrderedAddMonoid` `Nat.strictMono_cast` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero`
`summable_norm_sub_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.instNatCast` `Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Summable` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.instPow` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional`	—	`subsingleton_or_nontrivial` `Summable.of_finite` `Finite.of_subsingleton` `SummationFilter.instHasSupportOfLeAtTop` `SummationFilter.instLeAtTopUnconditional` `Summable.of_norm_bounded_eventually` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_norm_rpow` `AddSubgroup.isClosed_of_discrete` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.Finite.subset` `Set.Finite.preimage_embedding` `Metric.finite_isBounded_inter_isClosed` `FiniteDimensional.proper_real` `DiscreteTopology.isDiscrete` `Metric.isBounded_closedBall` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `dist_self` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `two_mul` `dist_zero_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Module.finrank_pos` `commRing_strongRankCondition` `Int.instNontrivial` `instModuleFinite_of_discrete_submodule` `Int.instIsDomain` `Module.IsReflexive.to_isTorsionFree` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `instModuleFree_of_discrete_submodule` `Real.rpow_lt_rpow_iff_of_neg` `mul_pos` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `lt_of_le_of_ne'` `norm_nonneg` `LT.lt.trans` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `Real.mul_rpow` `one_div` `abs_eq_self` `le_of_lt` `Real.rpow_pos_of_pos` `LE.le.trans_lt` `norm_sub_norm_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.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `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_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Submodule.addSubgroupClass` `AddSubgroupClass.coe_norm` `sub_lt_iff_lt_add'` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Mathlib.Meta.NormNum.isNat_lt_true`
`summable_norm_sub_zpow` 📖	mathematical	`Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `DivInvMonoid.toZPow` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional`	—	`Real.rpow_intCast` `summable_norm_sub_rpow` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`summable_norm_zpow` 📖	mathematical	`Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `DivInvMonoid.toZPow` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `SummationFilter.unconditional`	—	`sub_zero` `summable_norm_sub_zpow`
`tsumNormRPowBound_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `tsumNormRPowBound`	—	`exists_finsetSum_norm_rpow_le_tsum`
`tsumNormRPowBound_spec` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.instNatCast` `Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Real.instPow` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `Real.instMul` `tsumNormRPowBound` `tsum` `Real.pseudoMetricSpace` `Real.instAdd` `Real.instSub` `Real.instOne` `SummationFilter.unconditional`	—	`exists_finsetSum_norm_rpow_le_tsum`
`tsum_norm_rpow_le` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.instNatCast` `Module.finrank` `Submodule` `Int.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toIntModule` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.addCommGroup` `Int.instRing`	`Real.instLE` `tsum` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.instPow` `Norm.norm` `NormedAddCommGroup.toNorm` `Submodule.normedAddCommGroup` `SummationFilter.unconditional` `Real.instMul` `tsumNormRPowBound` `Real.instAdd` `Real.instSub` `Real.instOne`	—	`Summable.tsum_le_of_sum_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `SummationFilter.instNeBotUnconditional` `summable_norm_rpow` `tsumNormRPowBound_spec`

---

← Back to Index