InfiniteSum

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

Statistics

Metric	Count
Definitions	0
Theorems mul_norm, mul_of_nonneg, hasSum_sum_range_mul_of_summable_norm, hasSum_sum_range_mul_of_summable_norm', summable_mul_of_summable_norm, summable_mul_of_summable_norm', summable_norm_sum_mul_antidiagonal_of_summable_norm, summable_norm_sum_mul_range_of_summable_norm, summable_of_absolute_convergence_real, summable_sum_mul_antidiagonal_of_summable_norm', summable_sum_mul_range_of_summable_norm', tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm, tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm', tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm, tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm', tsum_mul_tsum_of_summable_norm, tsum_mul_tsum_of_summable_norm'	17
Total	17

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	of_nonneg_of_le norm_nonneg norm_mul_le mul_of_nonneg
mul_of_nonneg 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Pi.hasLe Real.instLE Pi.instZero Real.instZero	Real.instMul	—	summable_prod_of_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tsum_mul_left TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional mul_right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSum_sum_range_mul_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	HasSum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Finset.sum Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum	—	tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm Summable.hasSum Summable.of_norm summable_norm_sum_mul_range_of_summable_norm
hasSum_sum_range_mul_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	HasSum Finset.sum Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum	—	tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' Summable.hasSum summable_sum_mul_range_of_summable_norm'
summable_mul_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	Summable.of_norm Summable.mul_norm
summable_mul_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	hasSum_of_subseq_of_summable Summable.mul_norm Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.tendsto_finset_prod_atTop Filter.prod_atTop_atTop_eq Filter.Tendsto.prodMap Summable.hasSum Finset.sum_product Finset.sum_congr Filter.Tendsto.comp ContinuousAt.tendsto Continuous.continuousAt continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing nhds_prod_eq HasSum.summable
summable_norm_sum_mul_antidiagonal_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	summable_sum_mul_antidiagonal_of_summable_mul T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Summable.mul_of_nonneg norm_nonneg Summable.of_nonneg_of_le norm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_mul_le
summable_norm_sum_mul_range_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	Finset.Nat.sum_antidiagonal_eq_sum_range_succ summable_norm_sum_mul_antidiagonal_of_summable_norm
summable_of_absolute_convergence_real 📖	mathematical	Filter.Tendsto Real Finset.sum Real.instAddCommMonoid Finset.range abs Real.lattice Real.instAddGroup Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Summable SummationFilter.unconditional	—	Summable.of_norm Real.instCompleteSpace hasSum_iff_tendsto_nat_of_nonneg norm_nonneg
summable_sum_mul_antidiagonal_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	summable_sum_mul_antidiagonal_of_summable_mul T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing summable_mul_of_summable_norm'
summable_sum_mul_range_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Finset.sum Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	Finset.Nat.sum_antidiagonal_eq_sum_range_succ summable_sum_mul_antidiagonal_of_summable_norm'
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal	—	Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Summable.of_norm summable_mul_of_summable_norm
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal	—	Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing summable_mul_of_summable_norm'
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Finset.sum Finset.range	—	Finset.Nat.sum_antidiagonal_eq_sum_range_succ tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum Finset.sum Finset.range	—	Finset.Nat.sum_antidiagonal_eq_sum_range_succ tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'
tsum_mul_tsum_of_summable_norm 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	—	Summable.tsum_mul_tsum T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Summable.of_norm summable_mul_of_summable_norm
tsum_mul_tsum_of_summable_norm' 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedRing.toNorm SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing tsum	—	Summable.tsum_mul_tsum T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing summable_mul_of_summable_norm'

---

← Back to Index