Multiplication increases modified degree by at most ordinary degree

The key step is multiplication by one input variable. Interpolation handles a monomial that reaches the middle level, and majority is idempotent.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.span_map_mem {I : Type u_1} {V : Type u_2} {W : Type u_3} [AddCommMonoid V] [Module (ZMod 2) V] [AddCommMonoid W] [Module (ZMod 2) W] (v : I → V) (L : V →ₗ[ZMod 2] W) (U : Submodule (ZMod 2) W) (h : ∀ (i : I), L (v i) ∈ U) {f : V} (hf : f ∈ Submodule.span (ZMod 2) (Set.range v)) : L f ∈ U

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.majority_mul_mem {m : ℕ} (W : Submodule (ZMod 2) (Finset (Fin (2 * m + 1)) → ZMod 2)) (h : ∀ (a : Low (Fin (2 * m + 1)) m), atomEval (a, true) ∈ W) (f : Finset (Fin (2 * m + 1)) → ZMod 2) : (fun (x : Finset (Fin (2 * m + 1))) => majority x * f x) ∈ W

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.atom_variable_mem {m : ℕ} (a : Atom m) (j : Fin (2 * m + 1)) : (fun (x : Finset (Fin (2 * m + 1))) => monomial {j} x * atomEval a x) ∈ Submodule.span (ZMod 2) (Set.range fun (b : { b : Atom m // atomWeight b ≤ atomWeight a + 1 }) => atomEval ↑b)

def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.replaceFactor {k m : ℕ} (a : Term k m) (i : Fin k) : (Finset (Fin (2 * m + 1)) → ZMod 2) →ₗ[ZMod 2] BlockCube k m → ZMod 2

Insert a function into one factor of a product generator.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.replaceFactor_atom {k m : ℕ} (a : Term k m) (i : Fin k) (b : Atom m) : (replaceFactor a i) (atomEval b) = termEval (Function.update a i b)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.weight_update {k m : ℕ} (a : Term k m) (i : Fin k) (b : Atom m) : weight (Function.update a i b) = atomWeight b + ∑ j ∈ Finset.univ.erase i, atomWeight (a j)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.weight_eq {k m : ℕ} (a : Term k m) (i : Fin k) : weight a = atomWeight (a i) + ∑ j ∈ Finset.univ.erase i, atomWeight (a j)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.filtration_mono {k m r s : ℕ} (h : r ≤ s) : filtration k m r ≤ filtration k m s

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.term_mem {k m : ℕ} (a : Term k m) {r : ℕ} (h : weight a ≤ r) : termEval a ∈ filtration k m r

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.term_variable_mem {k m : ℕ} (a : Term k m) (i : Fin k) (j : Fin (2 * m + 1)) : (fun (x : BlockCube k m) => monomial {j} (x i) * termEval a x) ∈ filtration k m (weight a + 1)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.variable_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)) : (fun (x : BlockCube k m) => monomial {j} (x i) * f x) ∈ filtration k m (r + 1)

Multiplying by one variable increases the modified degree by at most one.