Dioph.pow_dioph
theorem Dioph.pow_dioph :
∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v ^ g v
This is a version of Matiyasevic's theorem. The theorem states that for any type `α` and any two functions `f` and `g` that map a function from `α` to natural numbers (`ℕ`) to a natural number, if `f` and `g` are both Diophantine functions (that is, their graphs are Diophantine), then the function that maps `v` to `f(v) ^ g(v)` (i.e., the natural number `f(v)` raised to the power of `g(v)`), is also a Diophantine function.
More concisely: If `f` and `g` are Diophantine functions mapping natural numbers to natural numbers, then their composition `x ↦ f x ^ g x` is also a Diophantine function.
|
Poly.isPoly
theorem Poly.isPoly : ∀ {α : Type u_1} (f : Poly α), IsPoly ⇑f
This theorem states that for any type `α` and for any multivariate integer polynomial `f` of type `α`, the function underlying `f` is a polynomial. Here, `IsPoly ⇑f` indicates that the function obtained by applying the 'dereference' or 'coercion' operator (`⇑`) to `f` satisfies the property of being a polynomial, which is what `IsPoly` checks for. This basically validates the definition of `Poly` as the type of multivariate integer polynomials.
More concisely: For any type `α` and any multivariate integer polynomial `f` of type `α`, the function `⇑f` is a polynomial.
|
Dioph.union
theorem Dioph.union : ∀ {α : Type u} {S S' : Set (α → ℕ)}, Dioph S → Dioph S' → Dioph (S ∪ S')
The theorem `Dioph.union` asserts that for any type `α` and any two sets `S` and `S'` of functions from `α` to natural numbers, if both `S` and `S'` are Diophantine, then their union `S ∪ S'` is also Diophantine. Here, a set is considered Diophantine if there exists a polynomial such that a function is in the set if and only if there exists a natural number satisfying the polynomial equation.
More concisely: If `S` and `S'` are sets of functions from a type `α` to natural numbers that are Diophantine, then their union `S ∪ S'` is also Diophantine.
|
Dioph.diophFn_vec
theorem Dioph.diophFn_vec :
∀ {n : ℕ} (f : Vector3 ℕ n → ℕ), Dioph.DiophFn f ↔ Dioph {v | f (v ∘ Fin2.fs) = v Fin2.fz}
The theorem `Dioph.diophFn_vec` states that for all natural numbers `n` and a function `f` that maps vectors of length `n` of natural numbers to natural numbers, the function `f` is Diophantine if and only if the set of all functions `v` such that `f` of `v` composed with the successor function equals `v` of the zero function is Diophantine. In simpler terms, a function `f` that takes a vector of natural numbers and returns a natural number is Diophantine exactly when there exists a polynomial such that for any function `v`, `v` is in the set precisely when the polynomial equals zero.
More concisely: A function mapping vectors of natural numbers to natural numbers is Diophantine if and only if the set of vectors `v` such that applying `f` to `v` and then the successor function equals the zero function is Diophantine in terms of the components of `v`.
|
Dioph.vec_ex1_dioph
theorem Dioph.vec_ex1_dioph : ∀ (n : ℕ) {S : Set (Vector3 ℕ n.succ)}, Dioph S → Dioph {v | ∃ x, Vector3.cons x v ∈ S}
The theorem `Dioph.vec_ex1_dioph` states that for any natural number `n` and for any Diophantine set `S` of vectors in `ℕ^(n+1)`, the set of vectors `v` in `ℕ^n` such that there exists a natural number `x` for which appending `x` to the front of `v` results in a vector in `S`, is also Diophantine. Thus, if a set of vectors (of size `n+1`) is Diophantine, then the set of all vectors that can be obtained by removing the first element from the vectors in the original set is also Diophantine.
More concisely: If `S` is a Diophantine set of vectors in `ℕ^(n+1)`, then the set of vectors in `ℕ^n` that can be extended to a vector in `S` is also Diophantine.
|
Dioph.eq_dioph
theorem Dioph.eq_dioph :
∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph fun v => f v = g v
This theorem states that for any two functions `f` and `g` from `α → ℕ` to `ℕ`, if both `f` and `g` are Diophantine (i.e., the set of natural numbers which can be represented by some polynomial equation), then the set of natural number sequences where `f` equals `g` is also Diophantine. In other words, the set of natural number sequences for which `f` and `g` yield the same result can also be represented by a polynomial equation.
More concisely: If `f` and `g` are Diophantine functions from `α` to `ℕ`, then the set `{n : ℕ | f(n) = g(n)}` is also Diophantine.
|
Dioph.reindex_dioph
theorem Dioph.reindex_dioph :
∀ {α : Type u} (β : Type u) {S : Set (α → ℕ)} (f : α → β), Dioph S → Dioph {v | v ∘ f ∈ S}
The theorem `Dioph.reindex_dioph` states that for any types `α` and `β`, and for any set `S` of functions from `α` to natural numbers, if `S` is Diophantine, then the set of functions `v` from `β` to natural numbers such that `(v ∘ f)` is in `S` is also Diophantine. Here, `f` is a function from `α` to `β`, and `v ∘ f` represents the function composition of `v` and `f`. This theorem essentially proves that the Diophantine property is preserved under re-indexing.
More concisely: If `S` is a Diophantine set of functions from `α` to natural numbers, then the set of functions `v` from `β` to natural numbers such that `(v ∘ f)` is in `S` for some function `f` from `α` to `β`, is also Diophantine.
|
Dioph.const_dioph
theorem Dioph.const_dioph : ∀ {α : Type} (n : ℕ), Dioph.DiophFn (Function.const (α → ℕ) n)
The theorem `Dioph.const_dioph` states that for any type `α` and natural number `n`, the constant function `Function.const (α → ℕ) n`, which takes any value from `α` and returns the constant `n`, is Diophantine. A function is considered Diophantine if its graph is Diophantine, meaning the set of its inputs and outputs can be expressed as the solutions to a Diophantine equation.
More concisely: The constant function from type `α` to natural numbers `Function.const (α → ℕ) n` is Diophantine for any type `α` and natural number `n`.
|
Poly.zero_apply
theorem Poly.zero_apply : ∀ {α : Type u_1} (x : α → ℕ), 0 x = 0
This theorem, `Poly.zero_apply`, states that for all types `α` and all functions `x` from `α` to the natural numbers `ℕ`, the application of the zero polynomial to `x` is zero. In mathematical terms, if you have a function `x` mapping any type `α` to the natural numbers, applying the zero polynomial to `x` will always yield zero, regardless of what `x` or `α` are.
More concisely: For all types `α` and functions `x` from `α` to the natural numbers, the zero polynomial applied to `x` equals zero.
|
Dioph.ex1_dioph
theorem Dioph.ex1_dioph : ∀ {α : Type u} {S : Set (Option α → ℕ)}, Dioph S → Dioph {v | ∃ x, Option.elim' x v ∈ S} := by
sorry
This theorem states that for any type `α` and any set `S` of functions from "Option of `α`" to `ℕ` (natural numbers), if `S` is Diophantine, then the set of functions `v` such that there exists an `x` of Option `α` for which `Option.elim' x v` is in `S` is also Diophantine. Here, a set is Diophantine if there exists a polynomial such that a function `v` is in the set if and only if there exists a tuple `t` of natural numbers such that the polynomial evaluated at `(v, t)` is zero. In the theorem, `Option.elim'` is a function that given an option value `x` and a function `v`, applies `v` to the value inside `x` if `x` is "some value", or returns a default value if `x` is "none".
More concisely: If `S` is a Diophantine set of functions from Option `α` to `ℕ`, then the set of functions `v` such that there exists an `x` of Option `α` with Option.elim' `x` `v` in `S` is also Diophantine.
|
Dioph.dioph_comp
theorem Dioph.dioph_comp :
∀ {α : Type} {n : ℕ} {S : Set (Vector3 ℕ n)},
Dioph S → ∀ (f : Vector3 ((α → ℕ) → ℕ) n), VectorAllP Dioph.DiophFn f → Dioph {v | (fun i => f i v) ∈ S}
The theorem `Dioph.dioph_comp` states that for any type `α`, natural number `n`, and set `S` of vectors of length `n` where each vector consists of natural numbers, if `S` is Diophantine then for any vector `f` where each element is a function from sequences of natural numbers to natural numbers and each of these functions is Diophantine, the set of sequences `v` for which the corresponding function values `(fun i => f i v)` are in `S` is also Diophantine. In other words, the theorem asserts that the composition of Diophantine functions yields a Diophantine set.
More concisely: If `S` is a Diophantine set of vectors of length `n` over natural numbers, and `f` is a function consisting of Diophantine functions from sequences of natural numbers to natural numbers, then the set of sequences `v` such that the function values `(fun i => f i v)` are in `S` is also Diophantine.
|
Poly.ext
theorem Poly.ext : ∀ {α : Type u_1} {f g : Poly α}, (∀ (x : α → ℕ), f x = g x) → f = g
The theorem `Poly.ext` states that for any type `α` and any two multivariate integer polynomials `f` and `g` of type `Poly α`, if `f` and `g` are equal for all functions from `α` to the natural numbers `ℕ`, then `f` is equal to `g`. This is an extensionality principle for the type of multivariate integer polynomials `Poly α`, asserting that two such polynomials are identical if they produce the same values for all possible inputs.
More concisely: If two multivariate integer polynomials of type `Poly α` have the same value for all functions from `α` to the natural numbers `ℕ`, then they are equal.
|
Dioph.add_dioph
theorem Dioph.add_dioph :
∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v + g v
The theorem `Dioph.add_dioph` states that for any type `α` and any two functions `f` and `g` that map from a function (which itself maps from `α` to natural numbers) to natural numbers, if both `f` and `g` are Diophantine functions, then the function that maps `v` to the sum of `f v` and `g v` is also a Diophantine function. In other words, the sum of two Diophantine functions is also a Diophantine function.
More concisely: If `f` and `g` are Diophantine functions mapping from a function to natural numbers, then their sum `v => f v + g v` is also a Diophantine function.
|
Dioph.lt_dioph
theorem Dioph.lt_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v < g v}
The theorem `Dioph.lt_dioph` states that for any type `α` and any two functions `f` and `g` from `α → ℕ` to `ℕ`, if `f` and `g` are both Diophantine functions (meaning their graphs are Diophantine sets), then the set of functions `v` such that `f v` is less than `g v` is also a Diophantine set. In other words, the set of all functions where the value of `f` at a given function is less than the value of `g` at the same function is Diophantine if `f` and `g` themselves are Diophantine. This is a property about the preservation of Diophantineness under the operation of "less than".
More concisely: If `f` and `g` are Diophantine functions from type `α` to `ℕ`, then the set {`v` | `f v` < `g v`} is a Diophantine set.
|
Dioph.ext
theorem Dioph.ext : ∀ {α : Type u} {S S' : Set (α → ℕ)}, Dioph S → (∀ (v : α → ℕ), v ∈ S ↔ v ∈ S') → Dioph S' := by
sorry
The theorem `Dioph.ext` states that for any type `α` and any two sets `S` and `S'` of functions from `α` to natural numbers, if the set `S` is Diophantine (i.e., there exists a polynomial on `α ⊕ β` such that a function `v` is in `S` if and only if there exists a function `t : ℕ^β` such that the polynomial applied to the sum of `v` and `t` is zero), and every function `v` is in `S` if and only if it is in `S'`, then the set `S'` is also Diophantine. In other words, a Diophantine property is preserved under set equivalence.
More concisely: If two sets of functions from a type to natural numbers have the same elements and one is Diophantine, then so is the other.
|
Dioph.proj_dioph_of_nat
theorem Dioph.proj_dioph_of_nat : ∀ {n : ℕ} (m : ℕ) [inst : Fin2.IsLT m n], Dioph.DiophFn fun v => v (Fin2.ofNat' m)
This theorem states that for all natural numbers 'n', given another natural number 'm' and a proof that 'm' is less than 'n' (denoted `Fin2.IsLT m n`), the function which maps a function `v` (from natural numbers to natural numbers) to its 'm-th' value (`v (Fin2.ofNat' m)`) is Diophantine. In simpler words, for any `m` less than `n`, the projection function that picks the `m`-th component of the function `v` is a Diophantine function.
More concisely: For all natural numbers n and m with m < n, the function that maps a function v from natural numbers to natural numbers to its m-th component v (Fin2.ofNat m) is a Diophantine function.
|
Dioph.inter
theorem Dioph.inter : ∀ {α : Type u} {S S' : Set (α → ℕ)}, Dioph S → Dioph S' → Dioph (S ∩ S')
The theorem `Dioph.inter` states that for any two sets `S` and `S'` of functions from a type `α` to natural numbers (`ℕ`), if both `S` and `S'` are Diophantine, then their intersection (`S ∩ S'`) is also Diophantine. Here, a set is said to be Diophantine if there exists a polynomial on `α ⊕ β` such that a function `v` belongs to the set if and only if there exists a function `t : ℕ^β` such that the polynomial evaluated at `(v, t)` equals zero.
More concisely: If `S` and `S'` are Diophantine sets of functions from type `α` to natural numbers, then their intersection `S ∩ S'` is also a Diophantine set.
|
Dioph.mul_dioph
theorem Dioph.mul_dioph :
∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v * g v
The theorem `Dioph.mul_dioph` states that for any type `α` and any two functions `f` and `g` from `(α → ℕ) → ℕ`, if both `f` and `g` are Diophantine functions (i.e., their graphs are Diophantine sets), then the function that maps each function `v` to the product of `f v` and `g v` is also a Diophantine function. In other words, the product of two Diophantine functions is also a Diophantine function.
More concisely: The product of two Diophantine functions is a Diophantine function.
|
Dioph.abs_poly_dioph
theorem Dioph.abs_poly_dioph : ∀ {α : Type u} (p : Poly α), Dioph.DiophFn fun v => (p v).natAbs
The theorem `Dioph.abs_poly_dioph` states that for any multivariate integer polynomial `p` of any type `α`, the function that maps a vector `v` to the absolute value of `p` at `v` is a Diophantine function. In other words, the graph of this function is a Diophantine set. Here, the absolute value of an integer is computed as defined by `Int.natAbs`, which returns its non-negative counterpart.
More concisely: The theorem `Dioph.abs_poly_dioph` asserts that the absolute value of a multivariate integer polynomial evaluated at a vector is a Diophantine function.
|
Dioph.le_dioph
theorem Dioph.le_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v ≤ g v}
The theorem `Dioph.le_dioph` states that for any type `α` and any two functions `f` and `g` from `α → ℕ` to `ℕ`, if both `f` and `g` are Diophantine functions (i.e., the graph of the function is Diophantine), then the set of all `v` such that `f v` is less than or equal to `g v` is also Diophantine. In other words, the inequality `f v ≤ g v` is Diophantine whenever `f` and `g` are Diophantine functions.
More concisely: If `f` and `g` are Diophantine functions from a type `α` to `ℕ`, then the set {`v` | `f v` ≤ `g v`} is Diophantine.
|
Dioph.diophFn_comp2
theorem Dioph.diophFn_comp2 :
∀ {α : Type} {f g : (α → ℕ) → ℕ},
Dioph.DiophFn f →
Dioph.DiophFn g →
∀ {h : ℕ → ℕ → ℕ},
(Dioph.DiophFn fun v => h (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))) → Dioph.DiophFn fun v => h (f v) (g v)
The theorem `Dioph.diophFn_comp2` states that for any type `α`, and any functions `f` and `g` that map a function from `α` to `ℕ` to `ℕ`, if `f` and `g` are Diophantine functions (i.e. their graphs are Diophantine sets), and if there exists another function `h` from `ℕ` to `ℕ` to `ℕ` that is also Diophantine when considering its inputs as a function from `Fin2` (finite set with 2 elements) to `ℕ`, then the composite function `h` which takes `f v` and `g v` as arguments is also a Diophantine function. In essence, it shows that the composition of Diophantine functions under certain conditions produces another Diophantine function.
More concisely: If `f` and `g` are Diophantine functions mapping `α → ℕ` to `ℕ`, and there exists a Diophantine function `h` mapping `ℕ → ℕ → ℕ`, then their composition `h (f x) (g x)` is also a Diophantine function.
|