Basic definitions for Pythagorean polynomial parametrizations

This file contains the shared definitions used by the Frisch--Vaserstein formalization setup.

def LeanPool.PythagoreanPolynomialParametrization.IsPythagoreanTriple (x y z : ℤ) : Prop

A triple of integers (x,y,z) is a Pythagorean triple if x² + y² = z².

Equations

• LeanPool.PythagoreanPolynomialParametrization.IsPythagoreanTriple x y z = (x ^ 2 + y ^ 2 = z ^ 2)

def LeanPool.PythagoreanPolynomialParametrization.pythagoreanTriples : Set (ℤ × ℤ × ℤ)

The set of all Pythagorean triples.

Equations

• LeanPool.PythagoreanPolynomialParametrization.pythagoreanTriples = {(x, y, z) : ℤ × ℤ × ℤ | LeanPool.PythagoreanPolynomialParametrization.IsPythagoreanTriple x y z}

def LeanPool.PythagoreanPolynomialParametrization.positivePythagoreanTriples : Set (ℤ × ℤ × ℤ)

The set of all positive Pythagorean triples (x,y,z > 0).

Equations

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

@[reducible, inline]

abbrev LeanPool.PythagoreanPolynomialParametrization.IntPoly (n : ℕ) : Type

Multivariate polynomials with integer coefficients in n variables.

Equations

• LeanPool.PythagoreanPolynomialParametrization.IntPoly n = MvPolynomial (Fin n) ℤ

@[reducible, inline]

abbrev LeanPool.PythagoreanPolynomialParametrization.RatPoly (n : ℕ) : Type

Multivariate polynomials with rational coefficients in n variables.

Equations

• LeanPool.PythagoreanPolynomialParametrization.RatPoly n = MvPolynomial (Fin n) ℚ

def LeanPool.PythagoreanPolynomialParametrization.IsIntValued {n : ℕ} (p : RatPoly n) : Prop

A rational-coefficient polynomial is integer-valued if it evaluates to an integer at every integer tuple.

Equations

• LeanPool.PythagoreanPolynomialParametrization.IsIntValued p = ∀ (a : Fin n → ℤ), ∃ (k : ℤ), (MvPolynomial.eval fun (i : Fin n) => ↑(a i)) p = ↑k

def LeanPool.PythagoreanPolynomialParametrization.IntValuedSubring (n : ℕ) : Subring (RatPoly n)

The paper's ring Int(ℤⁿ) of integer-valued rational polynomials, represented as a subring of ℚ[x₁, ..., xₙ].

Equations

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

@[reducible, inline]

abbrev LeanPool.PythagoreanPolynomialParametrization.IntegerValuedPoly (n : ℕ) : Type

The type of integer-valued rational polynomials in n variables.

Equations

• LeanPool.PythagoreanPolynomialParametrization.IntegerValuedPoly n = ↥(LeanPool.PythagoreanPolynomialParametrization.IntValuedSubring n)

noncomputable def LeanPool.PythagoreanPolynomialParametrization.intPolyEval {n : ℕ} (p : IntPoly n) (a : Fin n → ℤ) : ℤ

Evaluate an integer-coefficient polynomial at an integer tuple.

Equations

• LeanPool.PythagoreanPolynomialParametrization.intPolyEval p a = (MvPolynomial.eval a) p

noncomputable def LeanPool.PythagoreanPolynomialParametrization.ratPolyEval {n : ℕ} (p : RatPoly n) (a : Fin n → ℤ) : ℚ

Evaluate a rational-coefficient polynomial at an integer tuple.

Equations

• LeanPool.PythagoreanPolynomialParametrization.ratPolyEval p a = (MvPolynomial.eval fun (i : Fin n) => ↑(a i)) p

def LeanPool.PythagoreanPolynomialParametrization.IntPolyTupleParametrizes {n k : ℕ} (F : Fin k → IntPoly n) (S : Set (Fin k → ℤ)) : Prop

General k-tuple version of parametrization by one tuple of integer-coefficient polynomials, matching pyth.tex lines 104--116.

Equations

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

def LeanPool.PythagoreanPolynomialParametrization.IntValuedTupleParametrizes {n k : ℕ} (F : Fin k → RatPoly n) (S : Set (Fin k → ℤ)) : Prop

General k-tuple version of parametrization by one tuple of integer-valued polynomials, matching pyth.tex lines 104--116.

Equations

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

def LeanPool.PythagoreanPolynomialParametrization.FiniteIntPolyTupleParametrizes {m n k : ℕ} (F : Fin m → Fin k → IntPoly n) (S : Set (Fin k → ℤ)) : Prop

Parametrization by a finite number of k-tuples of integer-coefficient polynomials, matching pyth.tex lines 118--125.

Equations

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

def LeanPool.PythagoreanPolynomialParametrization.FiniteIntValuedTupleParametrizes {m n k : ℕ} (F : Fin m → Fin k → RatPoly n) (S : Set (Fin k → ℤ)) : Prop

Parametrization by a finite number of k-tuples of integer-valued polynomials, matching pyth.tex lines 118--125.

Equations

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

def LeanPool.PythagoreanPolynomialParametrization.IntPolyParametrizes {n : ℕ} (f g h : IntPoly n) (S : Set (ℤ × ℤ × ℤ)) : Prop

A triple of integer-coefficient polynomials parametrizes a set S ⊆ ℤ³ if S equals the image of the polynomial map ℤⁿ → ℤ³.

Equations

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

def LeanPool.PythagoreanPolynomialParametrization.IntValuedParametrizes {n : ℕ} (f g h : RatPoly n) (S : Set (ℤ × ℤ × ℤ)) : Prop

A triple of rational-coefficient polynomials parametrizes a set S ⊆ ℤ³ if each is integer-valued and S equals the image of the polynomial map.

Equations

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