prodigy.distribution.negative_values¶
Exact check whether a subtraction minuend - subtrahend can be negative on the support of a generating function.
The check works on the generating function before the subtraction and does not use marginals. Marginals are not enough for two reasons:
A marginal sums coefficients over the other variables. If coefficients may be negative (e.g. templates with parameters of unknown sign in invariant synthesis), terms on negative values can cancel in the marginal.
If the subtrahend has infinite support, as in x := x - y for a geometric y, the result has infinitely many negative powers of x. Its marginal is then the expansion of a rational function at infinity, which looks finite at x = 0 although the result has mass on negative values.
The question is a property of the support of function: it has a term minuend^a * subtrahend^b with a < b. With a fresh symbol t, the substitution minuend -> minuend * t, subtrahend -> subtrahend / t maps such a term to t^(a - b), so the subtraction is never negative if and only if the substituted function is a formal power series. A rational function in lowest terms is a power series if and only if its denominator does not vanish when all variables are 0: a denominator that does not vanish there is invertible in the power series ring, and a power series that is rational has, by the faithful flatness of the completion, a reduced denominator with a non-zero constant term. This needs no assumption on the signs of coefficients or parameters.
- can_be_negative(function, variables, minuend, subtrahend)[source]¶
Decides whether minuend - subtrahend is negative for some term of the formal power series function.
minuend and subtrahend are variables of function (from variables) or constants; parameters are all symbols that are not in variables. Parameters are treated as indeterminates, so the answer holds for all values of the parameters except for the roots of a non-zero expression.
- Return type:
- Returns:
True or False if the question is decided, None if it cannot be decided (e.g. the subtrahend is a parameter, or function is not rational in its variables, the subtrahend is a variable and the check of
_power_series_with_exponentials()fails).- Parameters:
- require_non_negative(negative, temp_var, minuend, subtrahend)[source]¶
Raises a ValueError unless the result negative of
can_be_negative()proves the subtraction safe.