Interpolation on the lower half of the Boolean cube

The restricted squarefree monomials form a triangular spanning family on every cardinality downset. This is the interpolation ingredient in the proof of Chattopadhyay--Hatami--Lee--Lovett--Tal--Viola.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.monomial_empty {ι : Type u_1} [DecidableEq ι] (x : Finset ι) : monomial ∅ x = 1

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.monomial_union {ι : Type u_1} [DecidableEq ι] (a b x : Finset ι) : monomial (a ∪ b) x = monomial a x * monomial b x

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.restricted_monomials_span {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (f : Low ι m → ZMod 2) : f ∈ Submodule.span (ZMod 2) (Set.range fun (a x : Low ι m) => monomial ↑a ↑x)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.low_interpolation {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (f : Low ι m → ZMod 2) : ∃ q ∈ lowSpan m, ∀ (x : Low ι m), q ↑x = f x

Every function on the lower cardinality downset has a low-degree interpolant.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.monomial_eq_prod {ι : Type u_1} [DecidableEq ι] (a x : Finset ι) : monomial a x = ∏ i ∈ a, monomial {i} x

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.monomial_compl {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a x : Finset ι) : monomial a xᶜ = ∑ b ∈ a.powerset, monomial b x

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.lowSpan_compl {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} {q : Finset ι → ZMod 2} (hq : q ∈ lowSpan m) : (fun (x : Finset ι) => q xᶜ) ∈ lowSpan m

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.majority_decomposition {m : ℕ} (f : Finset (Fin (2 * m + 1)) → ZMod 2) : ∃ q ∈ lowSpan m, ∃ r ∈ lowSpan m, f = q + fun (x : Finset (Fin (2 * m + 1))) => majority x * r x

A function on an odd Boolean block is q + majority * r, with both q and r spanned by monomials of degree at most half the block length.