Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The functions obtained from with are linearly independent, so they span a space of dimension
Statement
Fix . The functions obtained by restricting the multilinear monomials with are linearly independent. Consequently they span a vector space of dimension
Facts & Assumptions
Given: an integer with .
A multilinear polynomial agreeing with the zero function on the cube is the zero polynomial ( is multilinear, agrees with at every point of , is degree-nonincreasing when nonzero, and is the unique multilinear polynomial with that agreement).
The monomial expansion of a polynomial is unique (Monomials, coefficients, degree in each variable and total degree in ).
The subsets of of size at most number (The set of -element subsets and the binomial coefficient , The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition).
Proof
Suppose a linear combination of the restricted functions with vanishes on the whole cube. The same coefficients then define a multilinear polynomial vanishing on the cube, so [L1] makes that polynomial the zero polynomial.
By uniqueness of monomial expansion [F1], every coefficient in that polynomial is . Hence the restricted functions are linearly independent.
Their number is the sum in [F2], so the span has exactly that dimension.
Depends on
- Multilinear polynomials and the reduction $x_i^{2}\mapsto x_i$ on the cube
- $\widetilde f$ is multilinear, agrees with $f$ at every point of $\{0,1\}^{n}$, is degree-nonincreasing when nonzero, and is the unique multilinear polynomial with that agreement
- Monomials, coefficients, degree in each variable and total degree in $F[x_1,\dots,x_n]$
- Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i<n} \lambda_i v_i = 0_V$ forces every $\lambda_i = 0_F$, and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent
- Finite-dimensional vector space, and its dimension $\dim_F V$; infinite-dimensional means having no finite basis
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition
- The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form
- Vector space over a field
Used by
Dependency tree · two levels
54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- J. Matousek, Thirty-three Miniatures, Miniature 17 (standard reference, not scraped)