Rational hitting lists: small expansion

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/SmallExpansion.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

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

The coefficient realization of P_M(K), with its exact degree bound.

Equations

• Complexity.RationalHitting.SmallExpansion.polynomialMap M = (Polynomial.degreeLT K M).subtype ∘ₗ ↑(Polynomial.degreeLTEquiv K M).symm

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

@[simp]

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.SmallExpansion.polynomialMap_mem {K : Type u_1} [Field K] (M : ℕ) (x : Fin M → K) : (polynomialMap M) x ∈ Polynomial.degreeLT K M

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

• Complexity.RationalHitting.SmallExpansion.polynomialSpace V = Submodule.map (Complexity.RationalHitting.SmallExpansion.polynomialMap M) V

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

• Complexity.RationalHitting.SmallExpansion.taylorCoordinates M a = (Polynomial.degreeLTEquiv K M).symm.trans ((Polynomial.taylorLinearEquiv a M).trans (Polynomial.degreeLTEquiv K M))

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.SmallExpansion.reverseCoordinates {K : Type u_1} [Field K] (M : ℕ) : (Fin M → K) ≃ₗ[K] Fin M → K

Reverse the order of a finite coefficient vector.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RationalHitting.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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RationalHitting.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.