Small-subspace expansion

A subspace U of Fin M → K⸨X⸩ supported in the first N coordinates, of dimension 1 ≤ k ≤ B, expands under the reverse-Taylor tests at w distinct points of a characteristic zero field K: any common target subspace containing all w images has dimension greater than (w - 1) * k, as soon as M = N + 2 w³ B. The proof combines the order reversal rank inequality of LaurentReduction with the Wronskian order bound of Expansion.

Main definitions

• SmallExpansion.polynomialMap: coefficient vectors as polynomials of degree < M.
• SmallExpansion.polynomialSpace: the polynomial subspace of a coefficient subspace.
• SmallExpansion.taylorCoordinates, SmallExpansion.reverseCoordinates, SmallExpansion.reverseTaylorCoordinates: Taylor coordinates at a point, coordinate reversal, and reversed Taylor coordinates.
• SmallExpansion.testMap: the reverse-Taylor test at a point, weighting the j-th Taylor coordinate by X ^ j.

Main results

• SmallExpansion.order_reversal_sum: summed order reversal at a single point.
• SmallExpansion.small_expansion: the expansion inequality (w - 1) * finrank U < finrank W.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/SmallExpansion.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

noncomputable def Cslib.Circuits.Rational.SmallExpansion.polynomialMap {K : Type u_1} [Field K] (M : ℕ) : (Fin M → K) →ₗ[K] Polynomial K

Coefficient vectors of length M as polynomials of degree less than M.

theorem Cslib.Circuits.Rational.SmallExpansion.polynomialMap_injective {K : Type u_1} [Field K] (M : ℕ) : Function.Injective ⇑(polynomialMap M)

polynomialMap M is injective.

@[simp]

theorem Cslib.Circuits.Rational.SmallExpansion.polynomialMap_coeff {K : Type u_1} [Field K] (M : ℕ) (x : Fin M → K) (j : Fin M) : ((polynomialMap M) x).coeff ↑j = x j

For j : Fin M, the j-th coefficient of polynomialMap M x is x j.

theorem Cslib.Circuits.Rational.SmallExpansion.polynomialMap_mem {K : Type u_1} [Field K] (M : ℕ) (x : Fin M → K) : (polynomialMap M) x ∈ Polynomial.degreeLT K M

polynomialMap M x has degree strictly less than M.

theorem Cslib.Circuits.Rational.SmallExpansion.polynomialMap_coeff_high {K : Type u_1} [Field K] (M : ℕ) (x : Fin M → K) (j : ℕ) (hj : M ≤ j) : ((polynomialMap M) x).coeff j = 0

Every coefficient of polynomialMap M x of index j ≥ M is zero.

noncomputable def Cslib.Circuits.Rational.SmallExpansion.polynomialSpace {K : Type u_1} [Field K] {M : ℕ} (V : Submodule K (Fin M → K)) : Submodule K (Polynomial K)

The polynomial subspace corresponding to a subspace of coefficient vectors.

noncomputable def Cslib.Circuits.Rational.SmallExpansion.taylorCoordinates {K : Type u_1} [Field K] (M : ℕ) (a : K) : (Fin M → K) ≃ₗ[K] Fin M → K

Change coefficient vectors to Taylor coordinates at the specified point.

theorem Cslib.Circuits.Rational.SmallExpansion.taylorCoordinates_apply {K : Type u_1} [Field K] (M : ℕ) (a : K) (x : Fin M → K) (j : Fin M) : (taylorCoordinates M a) x j = ((Polynomial.taylor a) ((polynomialMap M) x)).coeff ↑j

The j-th Taylor coordinate of x at a is the j-th coefficient of taylor a (polynomialMap M x).

def Cslib.Circuits.Rational.SmallExpansion.reverseCoordinates {K : Type u_1} [Field K] (M : ℕ) : (Fin M → K) ≃ₗ[K] Fin M → K

Reverse the order of a finite coefficient vector.

noncomputable def Cslib.Circuits.Rational.SmallExpansion.reverseTaylorCoordinates {K : Type u_1} [Field K] (M : ℕ) (a : K) : (Fin M → K) ≃ₗ[K] Fin M → K

Take Taylor coordinates and reverse their order.

noncomputable def Cslib.Circuits.Rational.SmallExpansion.testMap {K : Type u_1} [Field K] (M : ℕ) (a : K) : (Fin M → LaurentReduction.F K) →ₗ[LaurentReduction.F K] Fin M → LaurentReduction.F K

The reverse-Taylor test on bounded-degree polynomials multiplies each Taylor coefficient by t^a and places it in output degree M-1-a.

theorem Cslib.Circuits.Rational.SmallExpansion.testMap_injective {K : Type u_1} [Field K] (M : ℕ) (a : K) : Function.Injective ⇑(testMap M a)

The reverse-Taylor test map testMap M a is injective.

theorem Cslib.Circuits.Rational.SmallExpansion.order_reversal_sum {K : Type u_1} [Field K] (M : ℕ) (a : K) (U W : Submodule (LaurentReduction.F K) (Fin M → LaurentReduction.F K)) (hW : Submodule.map (testMap M a) U ≤ W) {k l : ℕ} (b : Module.Basis (Fin k) K ↥(polynomialSpace (LaurentReduction.reducedSubspace U))) (c : Module.Basis (Fin l) K ↥(polynomialSpace (LaurentReduction.reducedSubspace W))) (hb : Function.Injective fun (j : Fin k) => Polynomial.rootMultiplicity a ↑(b j)) (hc : Function.Injective fun (j : Fin l) => Polynomial.rootMultiplicity a ↑(c j)) : k * (M - 1) ≤ ∑ j : Fin k, Polynomial.rootMultiplicity a ↑(b j) + ∑ j : Fin l, Polynomial.rootMultiplicity a ↑(c j)

Summation of order reversal, without selecting incompatible auxiliary subspaces: all inequalities concern the fixed filtration of the same W.

theorem Cslib.Circuits.Rational.SmallExpansion.small_expansion {K : Type u_1} [Field K] [CharZero K] (w B M N : ℕ) (hw : 1 ≤ w) (hN : 1 ≤ N) (hMN : M = N + 2 * w ^ 3 * B) (points : Fin w → K) (hp : Function.Injective points) (U W : Submodule (LaurentReduction.F K) (Fin M → LaurentReduction.F K)) (hU : ∀ x ∈ U, ∀ (j : Fin M), N ≤ ↑j → x j = 0) (hW : ∀ (i : Fin w), Submodule.map (testMap M (points i)) U ≤ W) (hk : 1 ≤ Module.finrank (LaurentReduction.F K) ↥U) (hkB : Module.finrank (LaurentReduction.F K) ↥U ≤ B) : (w - 1) * Module.finrank (LaurentReduction.F K) ↥U < Module.finrank (LaurentReduction.F K) ↥W

Small-subspace expansion in monomial coordinates in a common output space. The input subspace is restricted to degrees < N, not changed by padding.