Sum

class proveit.numbers.Sum(index_or_indices, summand, *, domain=None, domains=None, condition=None, conditions=None, styles=None, _lambda_map=None)

Bases: proveit.OperationOverInstances

Methods Summary

deduce_bound(self, summand_relation, …)	Given a universally quantified ordering relation over all summand instances, return a bounding relation for the summation. For example, using the summand relation forall_{k in {m…n}} (a(k) <= b(k)), we can prove sum_{l=m}^{n} a(l) <= sum_{l=m}^{n} b(l) or using the summand relation forall_{k in {m…n}} (a(k) < b(k)), and assuming m <= n, we can prove sum_{l=m}^{n} a(l) < sum_{l=m}^{n} b(l).
deduce_in_number_set(self, number_set, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
factorization(self, the_factors[, pull, …])	Return the proven factorization (equality with the factored form) from pulling the factor(s) from this summation to the “left” or “right”.
factorized(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘factorization’.
simplified(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘simplification’.

Methods Documentation

deduce_bound(self, summand_relation, \*\*defaults_config)

Given a universally quantified ordering relation over all summand instances, return a bounding relation for the summation. For example, using the summand relation

forall_{k in {m…n}} (a(k) <= b(k)),

we can prove

sum_{l=m}^{n} a(l) <= sum_{l=m}^{n} b(l)

or using the summand relation

forall_{k in {m…n}} (a(k) < b(k)),

and assuming m <= n, we can prove

sum_{l=m}^{n} a(l) < sum_{l=m}^{n} b(l)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_in_number_set(self, number_set, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

factorization(self, the_factors, pull='left', group_factors=True, group_remainder=None, \*\*defaults_config)

Return the proven factorization (equality with the factored form) from pulling the factor(s) from this summation to the “left” or “right”. If group_factors is True, the factors will be grouped together as a sub-product. group_remainder is not relevant kept for compatibility with other factor methods.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘factorized’ returns the right-hand side of ‘factorization’. ‘factor’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘factorization’ for the inner expression.

factorized(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘factorization’.

simplified(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘simplification’.