HexPolyTheory.Interpret

source

noncomputable def HexPolyTheory.Interpret.interpret {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (p : Hex.DensePoly E) :

Polynomial K

Interpret coefficients without identifying distinct stored nonzero values.

Equations

HexPolyTheory.Interpret.interpret f hz p = HexPolyTheory.toPolynomial (Hex.DensePoly.Interpret.map f hz p)

Instances For

source

theorem HexPolyTheory.Interpret.interpret_map {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (p : Hex.DensePoly E) :

interpret f hz p = toPolynomial (Hex.DensePoly.Interpret.map f hz p)

Expose the polynomial correspondence without unfolding its implementation.

source

@[simp]

theorem HexPolyTheory.Interpret.coeff_interpret {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (p : Hex.DensePoly E) (i : ℕ) :

(interpret f hz p).coeff i = f (p.coeff i)

source

@[simp]

theorem HexPolyTheory.Interpret.interpret_zero {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) :

interpret f hz 0 = 0

source

theorem HexPolyTheory.Interpret.interpret_eq_zero {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (p : Hex.DensePoly E) :

interpret f hz p = 0 ↔ p = 0

Zero reflection is sufficient; injectivity of the coefficient map is not needed.

source

@[simp]

theorem HexPolyTheory.Interpret.natDegree_interpret {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (p : Hex.DensePoly E) :

(interpret f hz p).natDegree = p.natDegree

source

@[simp]

theorem HexPolyTheory.Interpret.leadingCoeff_interpret {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (p : Hex.DensePoly E) :

(interpret f hz p).leadingCoeff = f p.leadingCoeff

source

theorem HexPolyTheory.Interpret.interpret_add {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Add E] (ha : ∀ (a b : E), f (a + b) = f a + f b) (p q : Hex.DensePoly E) :

interpret f hz (p + q) = interpret f hz p + interpret f hz q

source

theorem HexPolyTheory.Interpret.interpret_sub {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Sub E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (p q : Hex.DensePoly E) :

interpret f hz (p - q) = interpret f hz p - interpret f hz q

source

theorem HexPolyTheory.Interpret.interpret_neg {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Sub E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (p : Hex.DensePoly E) :

interpret f hz (-p) = -interpret f hz p

source

theorem HexPolyTheory.Interpret.monicize_leading {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Mul E] [Inv E] (hm : ∀ (a b : E), f (a * b) = f a * f b) (hi : ∀ (a : E), f a⁻¹ = (f a)⁻¹) (p : Hex.DensePoly E) (hp : p ≠ 0) :

(interpret f hz p.monicize).leadingCoeff = 1

A nonzero monicized representation has leading value one under interpretation.

source

theorem HexPolyTheory.Interpret.sub_isZero {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Sub E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (p q : Hex.DensePoly E) :

(p - q).isZero = true ↔ interpret f hz p = interpret f hz q

A zero difference decides semantic equality, even for unequal stored polynomials.

source

theorem HexPolyTheory.Interpret.interpret_mul {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Add E] [Mul E] (ha : ∀ (a b : E), f (a + b) = f a + f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : Hex.DensePoly E) :

interpret f hz (p * q) = interpret f hz p * interpret f hz q

source

theorem HexPolyTheory.Interpret.interpret_C {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (c : E) :

interpret f hz (Hex.DensePoly.C c) = Polynomial.C (f c)

Constant polynomials interpret their coefficient, including zero.

source

@[simp]

theorem HexPolyTheory.Interpret.interpret_one {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] (h1 : f 1 = 1) :

interpret f hz 1 = 1

source

theorem HexPolyTheory.Interpret.interpret_scale {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Mul E] (hm : ∀ (a b : E), f (a * b) = f a * f b) (c : E) (p : Hex.DensePoly E) :

interpret f hz (Hex.DensePoly.scale c p) = Polynomial.C (f c) * interpret f hz p

Scalar multiplication is interpreted coefficientwise.

source

theorem HexPolyTheory.Interpret.interpret_derivative {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [NatCast E] [Mul E] (hn : ∀ (n : ℕ), f ↑n = ↑n) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p : Hex.DensePoly E) :

interpret f hz p.derivative = Polynomial.derivative (interpret f hz p)

source

theorem HexPolyTheory.Interpret.eval_interpret {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [Add E] [Mul E] (ha : ∀ (a b : E), f (a + b) = f a + f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p : Hex.DensePoly E) (x : E) :

Polynomial.eval (f x) (interpret f hz p) = f (p.eval x)

source

theorem HexPolyTheory.Interpret.interpret_rem {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] [Add E] [Sub E] [Mul E] [Div E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : Hex.DensePoly E) :

interpret f hz (p.divMod q).2 = interpret f hz p % interpret f hz q

The interpreted remainder is Mathlib's remainder, including division by zero.

source

theorem HexPolyTheory.Interpret.interpret_mod {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] [Add E] [Sub E] [Mul E] [Div E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : Hex.DensePoly E) :

interpret f hz (p % q) = interpret f hz p % interpret f hz q

Polynomial modulus notation has the same interpreted remainder.

source

theorem HexPolyTheory.Interpret.interpret_divMod {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] [Add E] [Sub E] [Mul E] [Div E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : Hex.DensePoly E) :

(interpret f hz (p.divMod q).1, interpret f hz (p.divMod q).2) = (interpret f hz p / interpret f hz q, interpret f hz p % interpret f hz q)

Both division outputs agree with Mathlib, including a zero divisor.

source

theorem HexPolyTheory.Interpret.interpret_divModMonic {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] [Add E] [Sub E] [Mul E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (h1 : f 1 = 1) (p q : Hex.DensePoly E) (hq : q.Monic) :

(interpret f hz (p.divModMonic q hq).1, interpret f hz (p.divModMonic q hq).2) = (interpret f hz p / interpret f hz q, interpret f hz p % interpret f hz q)

The shared monic division corresponds to mathematical division without requiring an inverse or division operation on coefficient representatives.

source

theorem HexPolyTheory.Interpret.interpret_gcd {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] [Add E] [Sub E] [Mul E] [Div E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : Hex.DensePoly E) :

Associated (interpret f hz (p.gcd q)) (EuclideanDomain.gcd (interpret f hz p) (interpret f hz q))

The raw gcd is associated to Mathlib's normalized gcd.

source

theorem HexPolyTheory.Interpret.interpret_bezout {E : Type u} {K : Type v} [Zero E] [DecidableEq E] [Field K] [DecidableEq K] (f : E → K) (hz : ∀ (x : E), f x = 0 ↔ x = 0) [One E] [Add E] [Sub E] [Mul E] [Div E] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (hd : ∀ (a b : E), f (a / b) = f a / f b) (ha : ∀ (a b : E), f (a + b) = f a + f b) (h1 : f 1 = 1) (p q : Hex.DensePoly E) :

interpret f hz (p.xgcd q).left * interpret f hz p + interpret f hz (p.xgcd q).right * interpret f hz q = interpret f hz (p.xgcd q).gcd

The actual extended gcd supplies the interpreted Bézout identity.