The polynomial multiplication lemma

The ordinary total degree is Mathlib's MvPolynomial.totalDegree. Expanding over the polynomial's support avoids any assumptions about cancellation.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.variable_pow_mul_mem {k m r : ℕ} {f : BlockCube k m → ZMod 2} (hf : f ∈ filtration k m r) (i : Fin k) (j : Fin (2 * m + 1)) (d : ℕ) : (fun (x : BlockCube k m) => monomial {j} (x i) ^ d * f x) ∈ filtration k m (r + d)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.variable_prod_mul_mem {k m r : ℕ} {f : BlockCube k m → ZMod 2} (hf : f ∈ filtration k m r) (s : Finset (Fin k × Fin (2 * m + 1))) (e : Fin k × Fin (2 * m + 1) → ℕ) : (fun (x : BlockCube k m) => (∏ ij ∈ s, monomial {ij.2} (x ij.1) ^ e ij) * f x) ∈ filtration k m (r + ∑ ij ∈ s, e ij)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.polynomial_mul_mem {k m r : ℕ} {f : BlockCube k m → ZMod 2} (hf : f ∈ filtration k m r) (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) {d : ℕ} (hp : p.totalDegree ≤ d) : (fun (x : BlockCube k m) => polynomialEval p x * f x) ∈ filtration k m (r + d)

Multiplication by a degree-d polynomial increases modified degree by at most d.