Documentation

Mathlib.NumberTheory.Dioph

Diophantine functions and Matiyasevic's theorem #

Hilbert's tenth problem asked whether there exists an algorithm which for a given integer polynomial determines whether this polynomial has integer solutions. It was answered in the negative in 1970, the final step being completed by Matiyasevic who showed that the power function is Diophantine.

Here a function is called Diophantine if its graph is Diophantine as a set. A subset S ⊆ ℕ ^ α in turn is called Diophantine if there exists an integer polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

Main definitions #

Main statements #

References #

Tags #

Matiyasevic's theorem, Hilbert's tenth problem

TODO #

Multivariate integer polynomials #

Note that this duplicates MvPolynomial.

inductive IsPoly {α : Type u_1} :
((α))Prop

A predicate asserting that a function is a multivariate integer polynomial. (We are being a bit lazy here by allowing many representations for multiplication, rather than only allowing monomials and addition, but the definition is equivalent and this is easier to use.)

Instances For
    theorem IsPoly.neg {α : Type u_1} {f : (α)} :
    IsPoly fIsPoly (-f)
    theorem IsPoly.add {α : Type u_1} {f : (α)} {g : (α)} (hf : IsPoly f) (hg : IsPoly g) :
    IsPoly (f + g)
    def Poly (α : Type u) :

    The type of multivariate integer polynomials

    Equations
    Instances For
      instance Poly.instFunLike {α : Type u_1} :
      FunLike (Poly α) (α)
      Equations
      • Poly.instFunLike = { coe := Subtype.val, coe_injective' := }
      theorem Poly.isPoly {α : Type u_1} (f : Poly α) :
      IsPoly f

      The underlying function of a Poly is a polynomial

      theorem Poly.ext {α : Type u_1} {f : Poly α} {g : Poly α} :
      (∀ (x : α), f x = g x)f = g

      Extensionality for Poly α

      def Poly.proj {α : Type u_1} (i : α) :
      Poly α

      The ith projection function, x_i.

      Equations
      Instances For
        @[simp]
        theorem Poly.proj_apply {α : Type u_1} (i : α) (x : α) :
        (Poly.proj i) x = (x i)
        def Poly.const {α : Type u_1} (n : ) :
        Poly α

        The constant function with value n : ℤ.

        Equations
        Instances For
          @[simp]
          theorem Poly.const_apply {α : Type u_1} (n : ) (x : α) :
          (Poly.const n) x = n
          instance Poly.instZero {α : Type u_1} :
          Zero (Poly α)
          Equations
          instance Poly.instOne {α : Type u_1} :
          One (Poly α)
          Equations
          instance Poly.instNeg {α : Type u_1} :
          Neg (Poly α)
          Equations
          • Poly.instNeg = { neg := fun (f : Poly α) => -f, }
          instance Poly.instAdd {α : Type u_1} :
          Add (Poly α)
          Equations
          • Poly.instAdd = { add := fun (f g : Poly α) => f + g, }
          instance Poly.instSub {α : Type u_1} :
          Sub (Poly α)
          Equations
          • Poly.instSub = { sub := fun (f g : Poly α) => f - g, }
          instance Poly.instMul {α : Type u_1} :
          Mul (Poly α)
          Equations
          • Poly.instMul = { mul := fun (f g : Poly α) => f * g, }
          @[simp]
          theorem Poly.coe_zero {α : Type u_1} :
          0 = (Poly.const 0)
          @[simp]
          theorem Poly.coe_one {α : Type u_1} :
          1 = (Poly.const 1)
          @[simp]
          theorem Poly.coe_neg {α : Type u_1} (f : Poly α) :
          (-f) = -f
          @[simp]
          theorem Poly.coe_add {α : Type u_1} (f : Poly α) (g : Poly α) :
          (f + g) = f + g
          @[simp]
          theorem Poly.coe_sub {α : Type u_1} (f : Poly α) (g : Poly α) :
          (f - g) = f - g
          @[simp]
          theorem Poly.coe_mul {α : Type u_1} (f : Poly α) (g : Poly α) :
          (f * g) = f * g
          @[simp]
          theorem Poly.zero_apply {α : Type u_1} (x : α) :
          0 x = 0
          @[simp]
          theorem Poly.one_apply {α : Type u_1} (x : α) :
          1 x = 1
          @[simp]
          theorem Poly.neg_apply {α : Type u_1} (f : Poly α) (x : α) :
          (-f) x = -f x
          @[simp]
          theorem Poly.add_apply {α : Type u_1} (f : Poly α) (g : Poly α) (x : α) :
          (f + g) x = f x + g x
          @[simp]
          theorem Poly.sub_apply {α : Type u_1} (f : Poly α) (g : Poly α) (x : α) :
          (f - g) x = f x - g x
          @[simp]
          theorem Poly.mul_apply {α : Type u_1} (f : Poly α) (g : Poly α) (x : α) :
          (f * g) x = f x * g x
          instance Poly.instInhabited (α : Type u_4) :
          Equations
          instance Poly.instAddCommGroup {α : Type u_1} :
          Equations
          Equations
          • Poly.instAddGroupWithOne = let __src := inferInstance; AddGroupWithOne.mk SubNegMonoid.zsmul
          instance Poly.instCommRing {α : Type u_1} :
          Equations
          • Poly.instCommRing = let __spread.0 := inferInstance; let __spread.1 := inferInstance; CommRing.mk
          theorem Poly.induction {α : Type u_1} {C : Poly αProp} (H1 : ∀ (i : α), C (Poly.proj i)) (H2 : ∀ (n : ), C (Poly.const n)) (H3 : ∀ (f g : Poly α), C fC gC (f - g)) (H4 : ∀ (f g : Poly α), C fC gC (f * g)) (f : Poly α) :
          C f
          def Poly.sumsq {α : Type u_1} :
          List (Poly α)Poly α

          The sum of squares of a list of polynomials. This is relevant for Diophantine equations, because it means that a list of equations can be encoded as a single equation: x = 0 ∧ y = 0 ∧ z = 0 is equivalent to x^2 + y^2 + z^2 = 0.

          Equations
          Instances For
            theorem Poly.sumsq_nonneg {α : Type u_1} (x : α) (l : List (Poly α)) :
            0 (Poly.sumsq l) x
            theorem Poly.sumsq_eq_zero {α : Type u_1} (x : α) (l : List (Poly α)) :
            (Poly.sumsq l) x = 0 List.Forall (fun (a : Poly α) => a x = 0) l
            def Poly.map {α : Type u_4} {β : Type u_5} (f : αβ) (g : Poly α) :
            Poly β

            Map the index set of variables, replacing x_i with x_(f i).

            Equations
            Instances For
              @[simp]
              theorem Poly.map_apply {α : Type u_4} {β : Type u_5} (f : αβ) (g : Poly α) (v : β) :
              (Poly.map f g) v = g (v f)

              Diophantine sets #

              def Dioph {α : Type u} (S : Set (α)) :

              A set S ⊆ ℕ^α is Diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

              Equations
              Instances For
                theorem Dioph.ext {α : Type u} {S : Set (α)} {S' : Set (α)} (d : Dioph S) (H : ∀ (v : α), v S v S') :
                theorem Dioph.of_no_dummies {α : Type u} (S : Set (α)) (p : Poly α) (h : ∀ (v : α), S v p v = 0) :
                theorem Dioph.inject_dummies_lem {α : Type u} {β : Type u} {γ : Type u} (f : βγ) (g : γOption β) (inv : ∀ (x : β), g (f x) = some x) (p : Poly (α β)) (v : α) :
                (∃ (t : β), p (Sum.elim v t) = 0) ∃ (t : γ), (Poly.map (Sum.elim Sum.inl (Sum.inr f)) p) (Sum.elim v t) = 0
                theorem Dioph.inject_dummies {α : Type u} {β : Type u} {γ : Type u} {S : Set (α)} (f : βγ) (g : γOption β) (inv : ∀ (x : β), g (f x) = some x) (p : Poly (α β)) (h : ∀ (v : α), S v ∃ (t : β), p (Sum.elim v t) = 0) :
                ∃ (q : Poly (α γ)), ∀ (v : α), S v ∃ (t : γ), q (Sum.elim v t) = 0
                theorem Dioph.reindex_dioph {α : Type u} (β : Type u) {S : Set (α)} (f : αβ) :
                Dioph SDioph {v : β | v f S}
                theorem Dioph.DiophList.forall {α : Type u} (l : List (Set (α))) (d : List.Forall Dioph l) :
                Dioph {v : α | List.Forall (fun (S : Set (α)) => v S) l}
                theorem Dioph.inter {α : Type u} {S : Set (α)} {S' : Set (α)} (d : Dioph S) (d' : Dioph S') :
                Dioph (S S')
                theorem Dioph.union {α : Type u} {S : Set (α)} {S' : Set (α)} :
                Dioph SDioph S'Dioph (S S')
                def Dioph.DiophPFun {α : Type u} (f : (α) →. ) :

                A partial function is Diophantine if its graph is Diophantine.

                Equations
                Instances For
                  def Dioph.DiophFn {α : Type u} (f : (α)) :

                  A function is Diophantine if its graph is Diophantine.

                  Equations
                  Instances For
                    theorem Dioph.reindex_diophFn {α : Type u} {β : Type u} {f : (α)} (g : αβ) (d : Dioph.DiophFn f) :
                    Dioph.DiophFn fun (v : β) => f (v g)
                    theorem Dioph.ex_dioph {α : Type u} {β : Type u} {S : Set (α β)} :
                    Dioph SDioph {v : α | ∃ (x : β), Sum.elim v x S}
                    theorem Dioph.ex1_dioph {α : Type u} {S : Set (Option α)} :
                    Dioph SDioph {v : α | ∃ (x : ), Option.elim' x v S}
                    theorem Dioph.dom_dioph {α : Type u} {f : (α) →. } (d : Dioph.DiophPFun f) :
                    Dioph f.Dom
                    theorem Dioph.diophFn_iff_pFun {α : Type u} (f : (α)) :
                    theorem Dioph.abs_poly_dioph {α : Type u} (p : Poly α) :
                    Dioph.DiophFn fun (v : α) => (p v).natAbs
                    theorem Dioph.proj_dioph {α : Type u} (i : α) :
                    Dioph.DiophFn fun (v : α) => v i
                    theorem Dioph.diophPFun_comp1 {α : Type u} {S : Set (Option α)} (d : Dioph S) {f : (α) →. } (df : Dioph.DiophPFun f) :
                    Dioph {v : α | ∃ (h : f.Dom v), Option.elim' (f.fn v h) v S}
                    theorem Dioph.diophFn_comp1 {α : Type u} {S : Set (Option α)} (d : Dioph S) {f : (α)} (df : Dioph.DiophFn f) :
                    Dioph {v : α | Option.elim' (f v) v S}
                    theorem Dioph.diophFn_vec_comp1 {n : } {S : Set (Vector3 n.succ)} (d : Dioph S) {f : Vector3 n} (df : Dioph.DiophFn f) :
                    Dioph {v : Vector3 n | Vector3.cons (f v) v S}
                    theorem Dioph.vec_ex1_dioph (n : ) {S : Set (Vector3 n.succ)} (d : Dioph S) :
                    Dioph {v : Fin2 n | ∃ (x : ), Vector3.cons x v S}
                    theorem Dioph.diophFn_vec {n : } (f : Vector3 n) :
                    Dioph.DiophFn f Dioph {v : Fin2 (n + 1) | f (v Fin2.fs) = v Fin2.fz}
                    theorem Dioph.diophPFun_vec {n : } (f : Vector3 n →. ) :
                    Dioph.DiophPFun f Dioph {v : Fin2 (n + 1) | f.graph (v Fin2.fs, v Fin2.fz)}
                    theorem Dioph.diophFn_compn {α : Type} {n : } {S : Set (α Fin2 n)} :
                    Dioph S∀ {f : Vector3 ((α)) n}, VectorAllP Dioph.DiophFn fDioph {v : α | (Sum.elim v fun (i : Fin2 n) => f i v) S}
                    theorem Dioph.dioph_comp {α : Type} {n : } {S : Set (Vector3 n)} (d : Dioph S) (f : Vector3 ((α)) n) (df : VectorAllP Dioph.DiophFn f) :
                    Dioph {v : α | (fun (i : Fin2 n) => f i v) S}
                    theorem Dioph.diophFn_comp {α : Type} {n : } {f : Vector3 n} (df : Dioph.DiophFn f) (g : Vector3 ((α)) n) (dg : VectorAllP Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f fun (i : Fin2 n) => g i v
                    theorem Dioph.proj_dioph_of_nat {n : } (m : ) [Fin2.IsLT m n] :
                    Dioph.DiophFn fun (v : Vector3 n) => v (Fin2.ofNat' m)
                    theorem Dioph.const_dioph {α : Type} (n : ) :
                    theorem Dioph.dioph_comp2 {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {S : Prop} (d : Dioph fun (v : Vector3 2) => S (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))) :
                    Dioph fun (v : α) => S (f v) (g v)
                    theorem Dioph.diophFn_comp2 {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {h : } (d : Dioph.DiophFn fun (v : Vector3 2) => h (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))) :
                    Dioph.DiophFn fun (v : α) => h (f v) (g v)
                    theorem Dioph.eq_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph fun (v : α) => f v = g v
                    theorem Dioph.add_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f v + g v
                    theorem Dioph.mul_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f v * g v
                    theorem Dioph.le_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph {v : α | f v g v}
                    theorem Dioph.lt_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph {v : α | f v < g v}
                    theorem Dioph.ne_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph {v : α | f v g v}
                    theorem Dioph.sub_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f v - g v
                    theorem Dioph.dvd_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph fun (v : α) => f v g v
                    theorem Dioph.mod_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f v % g v
                    theorem Dioph.modEq_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {h : (α)} (dh : Dioph.DiophFn h) :
                    Dioph fun (v : α) => f v g v [MOD h v]
                    theorem Dioph.div_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f v / g v
                    theorem Dioph.pell_dioph :
                    Dioph fun (v : Vector3 4) => ∃ (h : 1 < v (Fin2.ofNat' 0)), Pell.xn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 2) Pell.yn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 3)
                    theorem Dioph.xn_dioph :
                    Dioph.DiophPFun fun (v : Vector3 2) => { Dom := 1 < v (Fin2.ofNat' 0), get := fun (h : 1 < v (Fin2.ofNat' 0)) => Pell.xn h (v (Fin2.ofNat' 1)) }
                    theorem Dioph.pow_dioph {α : Type} {f : (α)} {g : (α)} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) :
                    Dioph.DiophFn fun (v : α) => f v ^ g v

                    A version of Matiyasevic's theorem