Structures · Topology
SummationFilter.NeBot
Typeclass asserting that a summation filter is non-vacuous (if this is not satisfied, then every function is summable with every possible sum simultaneously).
- Shape
- One type argument · adds ne_bot
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
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 by109
- HasSum.tsum_eq
- HasProd.tprod_eq
- Summable.tsum_le_tsum
- HasSum.unique
- Summable.tsum_add
- Summable.sum_le_tsum
- hasSum_le
- Summable.hasSum_iff
- Summable.tsum_le_of_sum_le
- Measurable.tsum
- Summable.tsum_mul_left
- sum_le_hasSum
- Summable.le_tsum
- hasProd_le
- Multipliable.tprod_mul
- tsum_apply
- Summable.tsum_finsetSum
- Summable.tsum_lt_tsum
- le_hasSum
- Summable.map_tsum
- Multipliable.hasProd_iff
- HasSum.nonneg
- Summable.tsum_sub
- Summable.tsum_const_smul
- HasProd.unique
- ContinuousMap.tsum_apply
- Summable.tsum_mul_right
- Multipliable.map_tprod
- le_hasProd
- Summable.tsum_mono
- hasSum_lt
- ContinuousLinearMap.map_tsum
- prod_le_hasProd
- Summable.tsum_pos
- Multipliable.tprod_pow
- Complex.re_tsum
- hasSum_zero_iff_of_nonneg
- Measurable.tsum'
- Summable.tsum_eq_add_tsum_ite'
- Multipliable.tprod_lt_tprod
- AEMeasurable.tsum
- hasProd_lt
- RCLike.im_tsum
- tprod_eq_of_filter_le
- HasSum.nonpos
- SemiconjBy.tsum_left
- HasProd.le_one
- Commute.tsum_right
- MeasureTheory.StronglyMeasurable.tsum
- MeasureTheory.StronglyMeasurable.tprod
Ancestors0
No ancestors.