free_var_ranges

proveit.free_var_ranges(expr, exclusions=None)

Return the dictionary mapping Variables to forms w.r.t. ranges of indices (or solo) in which the variable occurs as free (not within a lambda map that parameterizes the base variable). Examples of “forms”:

x x_i x_1, …, x_n x_{i, 1}, …, x_{i, n_i} x_{1, 1}, …, x_{1, n_1}, ……, x_{m, 1}, …, x_{m, n_m}

For example, (x_1, …, x_n) -> x_1 + … + x_n + x_{n+1} would report {x_{n+1}} for the x entry but not x_1, …, x_n. In another example, (x_1, …, x_n) -> x_1 + … + x_k + x_{k+1} + … + x_{n} would report {x_1, …, x_k, x_{k+1}, …, x_{n}} for the x entry because the masking is not “explicit” and actually depends upon what may be assumed about k.

If this Expression is in the exclusion set, or contributes directly to a form that is in the exclusions set, skip over it. For example, given the expression

a*x_{i, 1} + … + a*x_{i, n_1}

if x_{i, 1}, …, x_{i, n_i} is in the exclusion set, then ‘a’ will be the only free variable reported.