OAI/Computability/RationalHitting/LaurentReduction.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RationalHitting.LaurentReduction.F line 11
  2. def OAI.RationalHitting.LaurentReduction.Integral line 14

    Source documentation

    Membership in K[[t]], inside K((t)).

    def Integral (x : F K) : Prop := ∃ p : PowerSeries K, HahnSeries.ofPowerSeries ℤ K p = x

    Mentions: OAI.RationalHitting.LaurentReduction.F

  3. def OAI.RationalHitting.LaurentReduction.reduction line 16
  4. def OAI.RationalHitting.LaurentReduction.reduce line 18
  5. lemma OAI.RationalHitting.LaurentReduction.integral_iff line 20
  6. lemma OAI.RationalHitting.LaurentReduction.integral_zero line 23
  7. lemma OAI.RationalHitting.LaurentReduction.integral_one line 24
  8. lemma OAI.RationalHitting.LaurentReduction.Integral.add line 25
  9. lemma OAI.RationalHitting.LaurentReduction.Integral.neg line 29
  10. lemma OAI.RationalHitting.LaurentReduction.Integral.sub line 32
  11. lemma OAI.RationalHitting.LaurentReduction.Integral.mul line 34
  12. lemma OAI.RationalHitting.LaurentReduction.reduction_zero line 39
  13. lemma OAI.RationalHitting.LaurentReduction.reduction_one line 40
  14. lemma OAI.RationalHitting.LaurentReduction.reduction_add line 41
  15. lemma OAI.RationalHitting.LaurentReduction.reduction_mul line 43
  16. lemma OAI.RationalHitting.LaurentReduction.normalize_vector line 55
  17. def OAI.RationalHitting.LaurentReduction.IntegralVector line 74

    Source documentation

    Coefficientwise integrality, not an arbitrary sublattice.

    def IntegralVector {ι : Type*} (x : ι → F K) : Prop := ∀ i, Integral (x i)

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.Integral

  18. lemma OAI.RationalHitting.LaurentReduction.IntegralVector.zero line 76
  19. lemma OAI.RationalHitting.LaurentReduction.IntegralVector.add line 77
  20. lemma OAI.RationalHitting.LaurentReduction.IntegralVector.sub line 80
  21. lemma OAI.RationalHitting.LaurentReduction.IntegralVector.smul line 83
  22. def OAI.RationalHitting.LaurentReduction.IntegralFunctional line 89

    Source documentation

    A coordinate functional which is defined integrally on the full ambient integral lattice.

    def IntegralFunctional {ι : Type*} (f : (ι → F K) →ₗ[F K] F K) : Prop :=
…

    Mentions: OAI.RationalHitting.LaurentReduction.F

  23. structure OAI.RationalHitting.LaurentReduction.IntegralFrame line 92
  24. theorem OAI.RationalHitting.LaurentReduction.exists_integralFrame line 105

    Source documentation

    Valuation-adapted Gaussian elimination constructs an integral frame for any Laurent-series subspace. The coordinate functionals guarantee saturation.

    theorem exists_integralFrame {ι : Type*} [Fintype ι]
    (U : Submodule (F K) (ι → F K)) : Nonempty (IntegralFrame U) := by
…

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.IntegralFrame

  25. lemma OAI.RationalHitting.LaurentReduction.IntegralFrame.linearIndependent line 213
  26. lemma OAI.RationalHitting.LaurentReduction.IntegralFrame.vector_mem line 221
  27. lemma OAI.RationalHitting.LaurentReduction.IntegralFrame.integral_coordinates line 226

    Source documentation

    Full integral-lattice saturation: every integral member has integral basis coordinates, explicitly given by the constructed functionals.

    lemma integral_coordinates (x : ι → F K) (hx : IntegralVector x) :
    ∀ j, Integral (b.coordinate j x) := fun j => b.coordinate_integral j x hx

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.IntegralVector, OAI.RationalHitting.LaurentReduction.Integral

  28. lemma OAI.RationalHitting.LaurentReduction.IntegralFrame.sum_coordinates line 229
  29. lemma OAI.RationalHitting.LaurentReduction.IntegralFrame.length_eq_finrank line 239
  30. lemma OAI.RationalHitting.LaurentReduction.integral_C line 246
  31. lemma OAI.RationalHitting.LaurentReduction.reduction_C line 249
  32. lemma OAI.RationalHitting.LaurentReduction.reduce_sum line 252
  33. lemma OAI.RationalHitting.LaurentReduction.reduce_smul line 257
  34. lemma OAI.RationalHitting.LaurentReduction.reduce_C_smul line 263
  35. def OAI.RationalHitting.LaurentReduction.ReducedSet line 271

    Source documentation

    The reduction uses every integral member of U.

    def ReducedSet {ι : Type*} (U : Submodule (F K) (ι → F K)) : Set (ι → K) :=
…

    Mentions: OAI.RationalHitting.LaurentReduction.F

  36. def OAI.RationalHitting.LaurentReduction.reducedSubspace line 274
  37. lemma OAI.RationalHitting.LaurentReduction.reducedSet_eq_span line 277
  38. lemma OAI.RationalHitting.LaurentReduction.reducedSubspace_eq_span line 302
  39. theorem OAI.RationalHitting.LaurentReduction.finrank_reducedSubspace line 308

    Source documentation

    Full integral reduction preserves dimension.

    theorem finrank_reducedSubspace {ι : Type*} [Fintype ι]
    (U : Submodule (F K) (ι → F K)) :
    finrank K (reducedSubspace U) = finrank (F K) U := by
…

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.reducedSubspace

  40. lemma OAI.RationalHitting.LaurentReduction.Integral.order_nonneg line 316
  41. lemma OAI.RationalHitting.LaurentReduction.Integral.order_eq_zero line 324
  42. def OAI.RationalHitting.LaurentReduction.weightMap line 329

    Source documentation

    Multiplication by t^a, written as its identical Laurent monomial.

    def weightMap {ι : Type*} (w : ι → ℕ) : (ι → F K) →ₗ[F K] (ι → F K) where
…

    Mentions: OAI.RationalHitting.LaurentReduction.F

  43. lemma OAI.RationalHitting.LaurentReduction.weightMap_injective line 334
  44. lemma OAI.RationalHitting.LaurentReduction.weighted_high_reduction_zero line 345

    Source documentation

    The key valuation step of order reversal: an integral normalized input having a nonzero low reduction cannot give a high leading output coefficient.

    lemma weighted_high_reduction_zero {ι : Type*} (w : ι → ℕ) (A : ℕ)
    (x : ι → F K) (hx : IntegralVector x)
    (hlow : ∃ j, w j ≤ A ∧ reduction (x j) ≠ 0)
    (c : F K) (hc : c ≠ 0)
    (hy : IntegralVector (c • weightMap w x)) :
    ∀ i, A < w i → reduction ((c • weightMap w x) i) = 0 := by
…

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.IntegralVector, OAI.RationalHitting.LaurentReduction.reduction, OAI.RationalHitting.LaurentReduction.weightMap

  45. theorem OAI.RationalHitting.LaurentReduction.reduction_weighted_supported line 372

    Source documentation

    Low coordinates detect reduction throughout U. This controls its full integral image lattice, not only the images of an arbitrary integral basis.

    theorem reduction_weighted_supported {ι : Type*} [Fintype ι]
    (w : ι → ℕ) (A : ℕ) (U : Submodule (F K) (ι → F K))
    (hdetect : ∀ x ∈ U, IntegralVector x →
      (∀ i, w i ≤ A → reduction (x i) = 0) → reduce x = 0)
    (y : ι → F K) (hyU : y ∈ U.map (weightMap w)) (hyI : IntegralVector y) :
    ∀ i, A < w i → reduction (y i) = 0 := by
…

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.IntegralVector, OAI.RationalHitting.LaurentReduction.reduction, OAI.RationalHitting.LaurentReduction.reduce, OAI.RationalHitting.LaurentReduction.weightMap

  46. lemma OAI.RationalHitting.LaurentReduction.exists_independent_subfamily line 401
  47. def OAI.RationalHitting.LaurentReduction.IntegralFrame.subframe line 421
  48. lemma OAI.RationalHitting.LaurentReduction.reducedSubspace_mono line 436
  49. theorem OAI.RationalHitting.LaurentReduction.exists_projection_subspace line 444

    Source documentation

    Choose an integral-lattice subspace on whose reduction a specified projection is injective, of dimension equal to that projection's rank.

    theorem exists_projection_subspace {ι : Type*} [Fintype ι]
    {V : Type*} [AddCommGroup V] [Module K V]
    (U : Submodule (F K) (ι → F K)) (P : (ι → K) →ₗ[K] V) :
    ∃ U' : Submodule (F K) (ι → F K), U' ≤ U ∧
      finrank (F K) U' = finrank K ((reducedSubspace U).map P) ∧
      ∀ x ∈ U', IntegralVector x → P (reduce x) = 0 → reduce x = 0 := by
…

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.reducedSubspace, OAI.RationalHitting.LaurentReduction.IntegralVector, OAI.RationalHitting.LaurentReduction.reduce

  50. def OAI.RationalHitting.LaurentReduction.lowProjection line 483

    Source documentation

    Low coordinate projection and its complementary support subspace.

    def lowProjection {ι : Type*} (w : ι → ℕ) (A : ℕ) :
    (ι → K) →ₗ[K] ({i : ι // w i ≤ A} → K) where
…
  51. def OAI.RationalHitting.LaurentReduction.lowSupported line 489
  52. lemma OAI.RationalHitting.LaurentReduction.finrank_map_injective line 495
  53. theorem OAI.RationalHitting.LaurentReduction.weighted_filtration_rank line 509

    Source documentation

    Filtration version of order reversal, before a constant coordinate change. This uses the whole integral lattice on both sides.

    theorem weighted_filtration_rank {ι : Type*} [Fintype ι]
    (w : ι → ℕ) (A : ℕ) (U : Submodule (F K) (ι → F K))
    (W : Submodule (F K) (ι → F K)) (hW : U.map (weightMap w) ≤ W) :
    finrank K ((reducedSubspace U).map (lowProjection w A)) ≤
      finrank K ↥(reducedSubspace W ⊓ lowSupported w A) := by
…

    Mentions: OAI.RationalHitting.LaurentReduction.F, OAI.RationalHitting.LaurentReduction.weightMap, OAI.RationalHitting.LaurentReduction.reducedSubspace, OAI.RationalHitting.LaurentReduction.lowProjection, OAI.RationalHitting.LaurentReduction.lowSupported

  54. def OAI.RationalHitting.LaurentReduction.liftMap line 534
  55. lemma OAI.RationalHitting.LaurentReduction.liftMap_apply line 537
  56. lemma OAI.RationalHitting.LaurentReduction.liftMap_comp line 543
  57. lemma OAI.RationalHitting.LaurentReduction.liftMap_id line 551
  58. lemma OAI.RationalHitting.LaurentReduction.liftMap_integral line 555
  59. lemma OAI.RationalHitting.LaurentReduction.reduction_liftMap line 563
  60. def OAI.RationalHitting.LaurentReduction.liftEquiv line 578
  61. lemma OAI.RationalHitting.LaurentReduction.liftEquiv_toLinearMap line 594
  62. lemma OAI.RationalHitting.LaurentReduction.liftEquiv_symm line 597
  63. lemma OAI.RationalHitting.LaurentReduction.integral_liftEquiv_iff line 602
  64. lemma OAI.RationalHitting.LaurentReduction.reducedSubspace_liftEquiv line 611
  65. def OAI.RationalHitting.LaurentReduction.conjugatedWeight line 631

    Source documentation

    Constant coordinates on the input and output may differ (Taylor on the input, reverse Taylor on the output in the application).

    def conjugatedWeight {ι : Type*} [Fintype ι] [DecidableEq ι]
    (Ein Eout : (ι → K) ≃ₗ[K] (ι → K)) (w : ι → ℕ) :
    (ι → F K) →ₗ[F K] (ι → F K) :=
…

    Mentions: OAI.RationalHitting.LaurentReduction.F

  66. lemma OAI.RationalHitting.LaurentReduction.conjugatedWeight_injective line 637
  67. theorem OAI.RationalHitting.LaurentReduction.conjugated_filtration_rank line 642
  68. lemma OAI.RationalHitting.LaurentReduction.finrank_map_add_finrank_inf_ker line 657