InfiniteSum

📁 Source: Mathlib/Analysis/Normed/Group/InfiniteSum.lean

Statistics

Metric	Count
Definitions	0
Theorems enorm_le_of_bounded, norm_le_of_bounded, of_nnnorm, of_nnnorm_bounded, of_norm, of_norm_bounded, of_norm_bounded_eventually, of_norm_bounded_eventually_nat, cauchySeq_finset_iff_vanishing_norm, cauchySeq_finset_of_norm_bounded, cauchySeq_finset_of_norm_bounded_eventually, cauchySeq_finset_of_summable_norm, cauchySeq_range_of_norm_bounded, enorm_tsum_le_tsum_enorm, hasSum_iff_tendsto_nat_of_summable_norm, hasSum_of_subseq_of_summable, nnnorm_tsum_le, norm_tsum_le_tsum_norm, summable_iff_vanishing_norm, tsum_of_enorm_bounded, tsum_of_nnnorm_bounded, tsum_of_norm_bounded	22
Total	22

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_le_of_bounded 📖	mathematical	HasSum ESeminormedAddCommMonoid.toAddCommMonoid SummationFilter.unconditional ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	le_of_tendsto_of_tendsto' OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotFinsetFilterOfNeBot SummationFilter.instNeBotUnconditional Filter.Tendsto.enorm enorm_sum_le_of_le
norm_le_of_bounded 📖	mathematical	HasSum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional Real Real.instAddCommMonoid Real.pseudoMetricSpace Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	—	le_of_tendsto_of_tendsto' OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotFinsetFilterOfNeBot SummationFilter.instNeBotUnconditional Filter.Tendsto.norm norm_sum_le_of_le

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_nnnorm 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SummationFilter.unconditional	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	of_nnnorm_bounded le_rfl
of_nnnorm_bounded 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	of_norm_bounded NNReal.summable_coe
of_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm SeminormedAddCommGroup.toNorm SummationFilter.unconditional	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	of_norm_bounded le_rfl
of_norm_bounded 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	summable_iff_cauchySeq_finset cauchySeq_finset_of_norm_bounded
of_norm_bounded_eventually 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	summable_iff_cauchySeq_finset cauchySeq_finset_of_norm_bounded_eventually
of_norm_bounded_eventually_nat 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Filter.atTop Nat.instPreorder	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	of_norm_bounded_eventually Nat.cofinite_eq_atTop

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_finset_iff_vanishing_norm 📖	mathematical	—	CauchySeq Finset PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialOrder.toPreorder Finset.partialOrder Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real Real.instLT Norm.norm SeminormedAddCommGroup.toNorm	—	cauchySeq_finset_iff_sum_vanishing SeminormedAddCommGroup.to_isUniformAddGroup Filter.HasBasis.forall_iff Metric.nhds_basis_ball ball_zero_eq
cauchySeq_finset_of_norm_bounded 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	CauchySeq Finset PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialOrder.toPreorder Finset.partialOrder Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	cauchySeq_finset_of_norm_bounded_eventually Filter.Eventually.of_forall
cauchySeq_finset_of_norm_bounded_eventually 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	CauchySeq Finset PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialOrder.toPreorder Finset.partialOrder Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	cauchySeq_finset_iff_vanishing_norm summable_iff_vanishing_norm Real.instCompleteSpace Set.Finite.mem_toFinset norm_sum_le_of_le le_abs_self Disjoint.mono_right le_sup_left
cauchySeq_finset_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm SeminormedAddCommGroup.toNorm SummationFilter.unconditional	CauchySeq Finset PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialOrder.toPreorder Finset.partialOrder Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	cauchySeq_finset_of_norm_bounded le_rfl
cauchySeq_range_of_norm_bounded 📖	mathematical	CauchySeq Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Nat.instPreorder Finset.sum Real.instAddCommMonoid Finset.range Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	CauchySeq PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Nat.instPreorder Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Finset.range	—	Metric.cauchySeq_iff' dist_eq_norm Finset.sum_Ico_eq_sub norm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_abs_self
enorm_tsum_le_tsum_enorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid tsum ESeminormedAddCommMonoid.toAddCommMonoid SummationFilter.unconditional ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace	—	tsum_of_enorm_bounded Summable.hasSum ENNReal.summable le_rfl
hasSum_iff_tendsto_nat_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm SeminormedAddCommGroup.toNorm SummationFilter.unconditional	HasSum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional Filter.Tendsto Finset.sum Finset.range Filter.atTop Nat.instPreorder nhds	—	HasSum.tendsto_sum_nat hasSum_of_subseq_of_summable Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.tendsto_finset_range
hasSum_of_subseq_of_summable 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm SeminormedAddCommGroup.toNorm SummationFilter.unconditional Filter.Tendsto Finset Filter.atTop PartialOrder.toPreorder Finset.partialOrder Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup nhds SeminormedAddCommGroup.toPseudoMetricSpace	HasSum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	tendsto_nhds_of_cauchySeq_of_subseq cauchySeq_finset_of_summable_norm
nnnorm_tsum_le 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace	—	tsum_of_nnnorm_bounded Summable.hasSum le_rfl
norm_tsum_le_tsum_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm SeminormedAddCommGroup.toNorm SummationFilter.unconditional	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional Real.instAddCommMonoid Real.pseudoMetricSpace	—	tsum_of_norm_bounded Summable.hasSum le_rfl
summable_iff_vanishing_norm 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional Finset Real Real.instLT Norm.norm SeminormedAddCommGroup.toNorm Finset.sum	—	summable_iff_cauchySeq_finset cauchySeq_finset_iff_vanishing_norm
tsum_of_enorm_bounded 📖	mathematical	HasSum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm ESeminormedAddCommMonoid.toESeminormedAddMonoid tsum ESeminormedAddCommMonoid.toAddCommMonoid SummationFilter.unconditional	—	HasSum.enorm_le_of_bounded Summable.hasSum tsum_eq_zero_of_not_summable enorm_zero ENNReal.instCanonicallyOrderedAdd
tsum_of_nnnorm_bounded 📖	mathematical	HasSum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	tsum_of_norm_bounded
tsum_of_norm_bounded 📖	mathematical	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional	—	HasSum.norm_le_of_bounded Summable.hasSum tsum_eq_zero_of_not_summable norm_zero ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotFinsetFilterOfNeBot SummationFilter.instNeBotUnconditional Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LE.le.trans norm_nonneg

---

← Back to Index