Structures · Topology
SummationFilter.LeAtTop
Typeclass asserting that a summation filter L is consistent with unconditional summation,
so that any unconditionally-summable function is L-summable with the same sum.
- Shape
- One type argument · adds le_atTop
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by76
- tsum_fintype
- tsum_eq_single
- hasSum_fintype
- Summable.sum_le_tsum
- tsum_eq_sum
- hasSum_single
- SummationFilter.support_eq_univ
- SummationFilter.LeAtTop.le_atTop
- tsum_ite_eq
- tprod_fintype
- sum_le_hasSum
- Summable.le_tsum
- Finset.hasProd
- hasSum_ite_eq
- Finset.hasSum
- hasSum_sum_of_ne_finset_zero
- tprod_eq_mulSingle
- Summable.tsum_lt_tsum
- le_hasSum
- tsum_eq_sum'
- hasProd_single
- tsum_eq_finsum
- tprod_eq_prod
- hasProd_ite_eq
- hasSum_ite_sub_hasSum
- HasSum.update
- hasProd_zero_of_exists_eq_zero
- le_hasProd
- hasSum_lt
- prod_le_hasProd
- tprod_eq_prod'
- HasProd.update
- Summable.tsum_pos
- hasProd_zero_zero
- multipliable_of_exists_eq_zero
- sum_eq_tsum_indicator
- hasSum_zero_iff_of_nonneg
- Summable.tsum_eq_add_tsum_ite'
- Multipliable.tprod_lt_tprod
- hasProd_lt
- hasProd_ite_div_hasProd
- HasSum.update'
- Multipliable.le_tprod
- prod_eq_tprod_mulIndicator
- hasProd_prod_of_ne_finset_one
- hasProd_one_iff_of_one_le
- hasSum_unique
- HasProd.update'
- hasProd_unique
- tprod_eq_finprod