noncomputable def UnbalancingLights.linearMonomial (k : ℕ) : Fin k →₀ ℕ

The linear monomial $x_0 x_1 \cdots x_{k-1}$, encoded as the exponent vector that is $1$ on every coordinate.

def UnbalancingLights.P_k (k : ℕ) : Set (MvPolynomial (Fin k) ℝ)

The class $\mathcal{P}_k$ of multivariate real polynomials in $k$ variables of total degree at most $k$, with all coefficients bounded by $1$ in absolute value, and whose coefficient at the linear monomial $x_1 \cdots x_k$ equals $1$.

theorem UnbalancingLights.inclusion_exclusion_identity {k : ℕ} (g : MvPolynomial (Fin k) ℝ) (hdeg : g.totalDegree ≤ k) : ∑ S : Finset (Fin k), (-1) ^ (k - S.card) * (MvPolynomial.eval fun (i : Fin k) => if i ∈ S then 1 else 0) g = MvPolynomial.coeff (linearMonomial k) g

Inclusion–exclusion identity: for a polynomial $g$ of total degree at most $k$ in $k$ variables, the alternating sum $\sum_{S \subseteq [k]} (-1)^{k - |S|} g(\mathbf{1}_S)$ equals the coefficient of $x_1 \cdots x_k$ in $g$.

theorem UnbalancingLights.exists_pos_lower_bound_eval_P_k (k : ℕ) (_hk : k ≥ 1) : ∃ c > 0, ∀ g ∈ P_k k, ∃ (p : Fin k → ℝ), (∀ (i : Fin k), p i ∈ Set.Icc 0 1) ∧ |(MvPolynomial.eval p) g| ≥ c

Lemma 2.5.3. For every $k \geq 1$ there is a constant $c > 0$ (here $c = 2^{-k}$) such that every polynomial $g \in \mathcal{P}_k$ attains absolute value at least $c$ at some point of $[0,1]^k$ (in fact at a vertex of the cube).