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.reverseTaylorCoordinates: Taylor coordinates at a point, in increasing and in reversed order.
• 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)

@[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

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

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

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.

theorem Cslib.Circuits.Rational.SmallExpansion.finrank_polynomialSpace {K : Type u_1} [Field K] {M : ℕ} (V : Submodule K (Fin M → K)) : Module.finrank K ↥(polynomialSpace V) = Module.finrank K ↥V

theorem Cslib.Circuits.Rational.SmallExpansion.polynomialSpace_bound {K : Type u_1} [Field K] {M : ℕ} (V : Submodule K (Fin M → K)) (f : Polynomial K) : f ∈ polynomialSpace V → f ≠ 0 → f.natDegree < M

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

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)

theorem Cslib.Circuits.Rational.SmallExpansion.map_taylor_projection_kernel {K : Type u_1} [Field K] (M : ℕ) (a : K) (A : ℕ) (V : Submodule K (Fin M → K)) : Submodule.map (polynomialMap M) (V ⊓ (LaurentReduction.lowProjection Fin.val A ∘ₗ ↑(taylorCoordinates M a)).ker) = Expansion.vanishingFiltration (polynomialSpace V) a (A + 1)

Kernel of the low Taylor projection is precisely the vanishing filtration.

theorem Cslib.Circuits.Rational.SmallExpansion.map_reverseTaylor_lowSupported {K : Type u_1} [Field K] (M : ℕ) (a : K) (A : ℕ) (V : Submodule K (Fin M → K)) : Submodule.map (polynomialMap M ∘ₗ ↑(reverseTaylorCoordinates M a).symm) (Submodule.map (↑(reverseTaylorCoordinates M a)) V ⊓ LaurentReduction.lowSupported Fin.val A) = Expansion.vanishingFiltration (polynomialSpace V) a (M - 1 - A)

The output-side low reverse coordinates mean high ordinary Taylor order.

theorem Cslib.Circuits.Rational.SmallExpansion.finrank_lowTaylor {K : Type u_1} [Field K] (M : ℕ) (a : K) (A : ℕ) (V : Submodule K (Fin M → K)) {h : ℕ} (b : Module.Basis (Fin h) K ↥(polynomialSpace V)) (hb : Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity a ↑(b j)) : Module.finrank K ↥(Submodule.map (LaurentReduction.lowProjection Fin.val A) (Submodule.map (↑(taylorCoordinates M a)) V)) = Fintype.card { j : Fin h // Polynomial.rootMultiplicity a ↑(b j) ≤ A }

theorem Cslib.Circuits.Rational.SmallExpansion.finrank_reverseTaylor {K : Type u_1} [Field K] (M : ℕ) (a : K) (A : ℕ) (V : Submodule K (Fin M → K)) {h : ℕ} (b : Module.Basis (Fin h) K ↥(polynomialSpace V)) (hb : Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity a ↑(b j)) : Module.finrank K ↥(Submodule.map (↑(reverseTaylorCoordinates M a)) V ⊓ LaurentReduction.lowSupported Fin.val A) = Fintype.card { j : Fin h // M - 1 - A ≤ Polynomial.rootMultiplicity a ↑(b j) }

theorem Cslib.Circuits.Rational.SmallExpansion.order_reversal_counts {K : Type u_1} [Field K] (M : ℕ) (a : K) (A : ℕ) (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)) : Fintype.card { j : Fin k // Polynomial.rootMultiplicity a ↑(b j) ≤ A } ≤ Fintype.card { j : Fin l // M - 1 - A ≤ Polynomial.rootMultiplicity a ↑(c j) }

The rank form of order reversal, at every threshold.

theorem Cslib.Circuits.Rational.SmallExpansion.sum_threshold_counts {h : ℕ} (d : Fin h → ℕ) (L : ℕ) : ∑ A ∈ Finset.range L, Fintype.card { j : Fin h // d j ≤ A } = ∑ j : Fin h, (L - d j)

Counting all thresholds counts each order with its exact multiplicity.

theorem Cslib.Circuits.Rational.SmallExpansion.sum_reversed_counts {h : ℕ} (d : Fin h → ℕ) (L : ℕ) (hd : ∀ (j : Fin h), d j ≤ L) : ∑ A ∈ Finset.range L, Fintype.card { j : Fin h // L - A ≤ d j } = ∑ j : Fin h, d j

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.sum_fin_val_le_square (h : ℕ) : ∑ j : Fin h, ↑j ≤ h * h

theorem Cslib.Circuits.Rational.SmallExpansion.expansion_numeric (w B M N k l : ℕ) (hw : 1 ≤ w) (hN : 1 ≤ N) (hMN : M = N + 2 * w ^ 3 * B) (hk : 1 ≤ k) (hkB : k ≤ B) (hh : w * (k * (M - 1)) ≤ k * (N - 1) + w * ∑ j : Fin k, ↑j + (l * (M - 1) + w * ∑ j : Fin l, ↑j)) : (w - 1) * k < l

theorem Cslib.Circuits.Rational.SmallExpansion.reduced_degree_bound {K : Type u_1} [Field K] {M N : ℕ} (U : Submodule (LaurentReduction.F K) (Fin M → LaurentReduction.F K)) (hU : ∀ x ∈ U, ∀ (j : Fin M), N ≤ ↑j → x j = 0) (f : Polynomial K) : f ∈ polynomialSpace (LaurentReduction.reducedSubspace U) → f ≠ 0 → f.natDegree < N

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.