OAI/Computability/RationalHitting/SmallExpansion.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RationalHitting.SmallExpansion.polynomialMap line 13

   Source documentation

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

   def polynomialMap (M : ℕ) : (Fin M → K) →ₗ[K] K[X] :=
   …

2. lemma OAI.RationalHitting.SmallExpansion.polynomialMap_injective line 16
3. lemma OAI.RationalHitting.SmallExpansion.polynomialMap_coeff line 19
4. lemma OAI.RationalHitting.SmallExpansion.polynomialMap_mem line 23
5. lemma OAI.RationalHitting.SmallExpansion.polynomialMap_coeff_high line 27
6. def OAI.RationalHitting.SmallExpansion.polynomialSpace line 32
7. lemma OAI.RationalHitting.SmallExpansion.finrank_polynomialSpace line 35
8. lemma OAI.RationalHitting.SmallExpansion.polynomialSpace_bound line 39
9. def OAI.RationalHitting.SmallExpansion.taylorCoordinates line 44
10. lemma OAI.RationalHitting.SmallExpansion.taylorCoordinates_apply line 48
11. def OAI.RationalHitting.SmallExpansion.reverseCoordinates line 51
12. def OAI.RationalHitting.SmallExpansion.reverseTaylorCoordinates line 59
13. def OAI.RationalHitting.SmallExpansion.testMap line 64

    Source documentation

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

    def testMap (M : ℕ) (a : K) : (Fin M → F K) →ₗ[F K] (Fin M → F K) :=
    …

14. lemma OAI.RationalHitting.SmallExpansion.testMap_injective line 67
15. lemma OAI.RationalHitting.SmallExpansion.map_taylor_projection_kernel line 71

    Source documentation

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

    lemma map_taylor_projection_kernel (M : ℕ) (a : K) (A : ℕ)
        (V : Submodule K (Fin M → K)) :
        (V ⊓ ((lowProjection Fin.val A).comp (taylorCoordinates M a).toLinearMap).ker).map
          (polynomialMap M) = vanishingFiltration (polynomialSpace V) a (A+1) := by
    …

    Mentions: OAI.RationalHitting.SmallExpansion.taylorCoordinates, OAI.RationalHitting.SmallExpansion.polynomialMap, OAI.RationalHitting.SmallExpansion.polynomialSpace

16. lemma OAI.RationalHitting.SmallExpansion.map_reverseTaylor_lowSupported line 94

    Source documentation

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

    lemma map_reverseTaylor_lowSupported (M : ℕ) (a : K) (A : ℕ)
        (V : Submodule K (Fin M → K)) :
        ((V.map (reverseTaylorCoordinates M a).toLinearMap) ⊓ lowSupported Fin.val A).map
          ((polynomialMap M).comp (reverseTaylorCoordinates M a).symm.toLinearMap) =
          vanishingFiltration (polynomialSpace V) a (M-1-A) := by
    …

    Mentions: OAI.RationalHitting.SmallExpansion.reverseTaylorCoordinates, OAI.RationalHitting.SmallExpansion.polynomialMap, OAI.RationalHitting.SmallExpansion.polynomialSpace

17. lemma OAI.RationalHitting.SmallExpansion.finrank_lowTaylor line 117
18. lemma OAI.RationalHitting.SmallExpansion.finrank_reverseTaylor line 140
19. theorem OAI.RationalHitting.SmallExpansion.order_reversal_counts line 151

    Source documentation

    The rank form of order reversal, at every threshold.

    theorem order_reversal_counts (M : ℕ) (a : K) (A : ℕ)
        (U W : Submodule (F K) (Fin M → F K)) (hW : U.map (testMap M a) ≤ W)
        {k l : ℕ} (b : Basis (Fin k) K (polynomialSpace (reducedSubspace U)))
        (c : Basis (Fin l) K (polynomialSpace (reducedSubspace W)))
        (hb : Function.Injective (fun j => (b j : K[X]).rootMultiplicity a))
        (hc : Function.Injective (fun j => (c j : K[X]).rootMultiplicity a)) :
        Fintype.card {j : Fin k // (b j : K[X]).rootMultiplicity a ≤ A} ≤
          Fintype.card {j : Fin l // M-1-A ≤ (c j : K[X]).rootMultiplicity a} := by
    …

    Mentions: OAI.RationalHitting.SmallExpansion.testMap, OAI.RationalHitting.SmallExpansion.polynomialSpace

20. lemma OAI.RationalHitting.SmallExpansion.sum_threshold_counts line 164

    Source documentation

    Counting all thresholds counts each order with its exact multiplicity.

    lemma sum_threshold_counts {h : ℕ} (d : Fin h → ℕ) (L : ℕ) :
        (∑ A ∈ Finset.range L, Fintype.card {j : Fin h // d j ≤ A}) =
          ∑ j, (L - d j) := by
    …

21. lemma OAI.RationalHitting.SmallExpansion.sum_reversed_counts line 179
22. theorem OAI.RationalHitting.SmallExpansion.order_reversal_sum line 194

    Source documentation

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

    theorem order_reversal_sum (M : ℕ) (a : K)
        (U W : Submodule (F K) (Fin M → F K)) (hW : U.map (testMap M a) ≤ W)
        {k l : ℕ} (b : Basis (Fin k) K (polynomialSpace (reducedSubspace U)))
        (c : Basis (Fin l) K (polynomialSpace (reducedSubspace W)))
        (hb : Function.Injective (fun j => (b j : K[X]).rootMultiplicity a))
        (hc : Function.Injective (fun j => (c j : K[X]).rootMultiplicity a)) :
        k * (M-1) ≤ (∑ j, (b j : K[X]).rootMultiplicity a) +
          (∑ j, (c j : K[X]).rootMultiplicity a) := by
    …

    Mentions: OAI.RationalHitting.SmallExpansion.testMap, OAI.RationalHitting.SmallExpansion.polynomialSpace

23. lemma OAI.RationalHitting.SmallExpansion.sum_fin_val_le_square line 232
24. lemma OAI.RationalHitting.SmallExpansion.expansion_numeric line 237
25. lemma OAI.RationalHitting.SmallExpansion.reduced_degree_bound line 281
26. theorem OAI.RationalHitting.SmallExpansion.small_expansion line 304

    Source documentation

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

    theorem small_expansion [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 (F K) (Fin M → F K))
        (hU : ∀ x ∈ U, ∀ j : Fin M, N ≤ j.val → x j = 0)
        (hW : ∀ i, U.map (testMap M (points i)) ≤ W)
        (hk : 1 ≤ finrank (F K) U) (hkB : finrank (F K) U ≤ B) :
        (w-1) * finrank (F K) U < finrank (F K) W := by
    …

    Mentions: OAI.RationalHitting.SmallExpansion.testMap