Commit 2025-10-06 12:30 abf8c9d3

View on Github →

feat(Topology/Algebra/InfiniteSum): generalise to allow summation filters (#29914) We introduce a notion of a "summation filter" on a type, which is (a structure wrapper around) a filter on the finsets of that type. Then we can define tsums / tprods "along L" for any summation filter L, giving a formalism that specializes to the existing notion of unconditional summation, but also covers conditional summation on ℕ etc. This is implemented using an optional parameter to HasSum, tsum etc which defaults to the standard unconditional sum, so the vast majority of existing code using unconditional summation will work without change. Co-authored by Chris Birkbeck.

Estimated changes

modified theorem Complex.conj_tsum
modified theorem Complex.hasSum_conj'
modified theorem Complex.hasSum_conj
modified theorem Complex.hasSum_im
modified theorem Complex.hasSum_ofReal
modified theorem Complex.hasSum_re
modified theorem Complex.im_tsum
modified theorem Complex.ofReal_tsum
modified theorem Complex.re_tsum
modified theorem Complex.summable_ofReal
modified theorem RCLike.conj_tsum
modified theorem RCLike.hasSum_conj'
modified theorem RCLike.hasSum_conj
modified theorem RCLike.hasSum_im
modified theorem RCLike.hasSum_ofReal
modified theorem RCLike.hasSum_re
modified theorem RCLike.im_tsum
modified theorem RCLike.ofReal_tsum
modified theorem RCLike.re_tsum
modified theorem RCLike.summable_conj
modified theorem RCLike.summable_ofReal
modified theorem Quaternion.hasSum_coe
modified theorem Quaternion.summable_coe
modified theorem Quaternion.tsum_coe
modified theorem HasProd.congr_fun
modified theorem HasProd.mul
modified theorem HasProd.update'
modified theorem Multipliable.congr
modified theorem Multipliable.map_tprod
modified theorem Multipliable.mul
modified theorem Multipliable.of_finite
modified theorem eq_mul_of_hasProd_ite
modified theorem hasProd_empty
modified theorem hasProd_ite_eq
modified theorem hasProd_one
modified theorem hasProd_single
modified theorem hasProd_unique
modified theorem multipliable_congr
modified theorem multipliable_empty
modified theorem multipliable_one
modified theorem multipliable_prod
modified theorem prod_eq_tprod_mulIndicator
modified theorem tprod_congr₂
modified theorem tprod_empty
modified theorem tprod_eq_finprod
modified theorem tprod_eq_mulSingle
modified theorem tprod_eq_prod'
modified theorem tprod_eq_prod
modified theorem tprod_fintype
modified theorem tprod_ite_eq
modified theorem tprod_of_exists_eq_zero
modified theorem tprod_one
modified theorem tprod_tprod_eq_mulSingle
modified theorem HasProd.prodMk
modified theorem HasSum.op
modified theorem HasSum.star
modified theorem HasSum.unop
modified theorem Pi.multipliable
modified theorem Summable.ofStar
modified theorem Summable.op
modified theorem Summable.star
modified theorem Summable.unop
modified theorem hasSum_op
modified theorem summable_op
modified theorem summable_star_iff'
modified theorem summable_star_iff
modified theorem summable_unop
modified theorem tprod_apply
modified theorem tsum_op
modified theorem tsum_star
modified theorem tsum_unop
added theorem Finset.hasProd_support
modified theorem HasProd.multipliable
modified theorem HasProd.tprod_eq
modified theorem HasProd.unique
modified def HasProd
modified theorem Multipliable.hasProd
modified theorem Multipliable.hasProd_iff
modified def Multipliable
added theorem hasProd_bot
modified theorem hasProd_fintype
added theorem multipliable_bot
added theorem tprod_bot
modified theorem HasProd.div
modified theorem HasProd.inv
modified theorem HasProd.update
modified theorem Multipliable.div
modified theorem Multipliable.inv
modified theorem Multipliable.of_inv
modified theorem Multipliable.trans_div
modified theorem Multipliable.update
modified theorem hasProd_ite_div_hasProd
modified theorem multipliable_inv_iff
modified theorem tprod_inv
modified theorem Summable.toCompl_tsum
modified theorem HasSum.const_smul
modified theorem HasSum.smul_const
modified theorem Summable.const_smul
modified theorem Summable.smul_const
modified theorem HasProd.le_one
modified theorem HasProd.one_le
modified theorem hasProd_le
modified theorem hasProd_le_of_prod_le
modified theorem hasProd_lt
modified theorem hasProd_mono
modified theorem hasProd_one_iff_of_one_le
modified theorem le_hasProd
modified theorem le_hasProd_of_le_prod
modified theorem lt_hasProd
modified theorem one_le_tprod
modified theorem prod_le_hasProd
modified theorem tprod_le_of_prod_le'
modified theorem tprod_le_one
modified theorem Commute.tsum_left
modified theorem Commute.tsum_right
modified theorem HasSum.const_div
modified theorem HasSum.div_const
modified theorem HasSum.mul_left
modified theorem HasSum.mul_right
modified theorem Summable.const_div
modified theorem Summable.div_const
modified theorem Summable.mul_left
modified theorem Summable.mul_right
modified theorem hasSum_div_const_iff
modified theorem hasSum_mul_left_iff
modified theorem hasSum_mul_right_iff
modified theorem summable_const_div_iff
modified theorem summable_div_const_iff
modified theorem summable_mul_left_iff
modified theorem summable_mul_right_iff
modified theorem tsum_div_const
modified theorem tsum_mul_left
modified theorem tsum_mul_right
added structure SummationFilter
modified theorem HasSum.matrix_diag
modified theorem HasSum.matrix_diagonal
modified theorem HasSum.matrix_transpose
modified theorem Matrix.transpose_tsum
modified theorem Summable.matrix_blockDiag'
modified theorem Summable.matrix_blockDiag
modified theorem Summable.matrix_diag
modified theorem Summable.matrix_diagonal
modified theorem Summable.matrix_transpose
modified theorem NNReal.coe_tsum
modified theorem NNReal.hasSum_coe
modified theorem NNReal.summable_coe