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 📖	—	HasSum ESeminormedAddCommMonoid.toAddCommMonoid SummationFilter.unconditional ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace 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 📖	—	HasSum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SummationFilter.unconditional Real Real.instAddCommMonoid Real.pseudoMetricSpace 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 instSemiringNNReal NNReal.instTopologicalSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SummationFilter.unconditional	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	of_nnnorm_bounded le_rfl
of_nnnorm_bounded 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNReal.instTopologicalSpace SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	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	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	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	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	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	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	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	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	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 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 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 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	SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	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 SeminormedAddCommGroup.toPseudoMetricSpace 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	—	tendsto_nhds_of_cauchySeq_of_subseq cauchySeq_finset_of_summable_norm
nnnorm_tsum_le 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNReal.instTopologicalSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup SummationFilter.unconditional	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	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.instLE tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	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 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	tsum ESeminormedAddCommMonoid.toAddCommMonoid	—	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 instSemiringNNReal NNReal.instTopologicalSpace SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	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	tsum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	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