Grace/Cumulus/Algebra/Polynomial/HornerPolynomial.g17

Open in Workbench Download source

Imports

HornerRoots · Assignment · Constants

Declarations

Source

1-- Horner coefficient lists as sparse polynomials, with evaluation compatibility.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.HornerPolynomial8import HornerRoots9import Assignment10import Constants1112-- The result is an element of the finite-support polynomial ring.13def polynomialFromHorner (I A add z neg mul one j leading : Set) (cs : List(A)) : Set :=14  monicValue{A}(polynomialCoefficients(I, A, z), polynomialAdd(I, A, add, z, neg, mul, one), polynomialMul(I, A, add, z, neg, mul, one), polynomialConstant(I, A, z, leading), polynomialVariable(I, A, z, one, j), cs)1516notation scoped polynomialFromHorner(I, R, j, leading, cs) => polynomialFromHorner(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, leading, cs)1718theorem polynomialFromHorner.nil (I A add z neg mul one j leading : Set)19  shows polynomialFromHorner(I, A, add, z, neg, mul, one, j, leading, []) = polynomialConstant(I, A, z, leading)20proof21  unfold polynomialFromHorner22  rw monicValue23  rfl2425section Rings26variable (I A add z neg mul one j leading : Set)27notation ring R := (A, add, z, neg, mul, one)28notation ring P := R[I]29hypothesis ring : IsCommRing(R)30hypothesis initial : leading ∈ R3132theorem polynomialFromHorner.member (cs : List(A))33  shows polynomialFromHorner(I, R, j, leading, cs) ∈ P34proof35  have ordinary := IsCommRing.ring with ring36  have zeroIn := IsRing.zero_in_carrier with ordinary37  have monoid := IsRing.multiplicative with ordinary38  have oneIn := IsMonoid.unit_in_carrier with monoid39  have variable := polynomialVariable.member at I, A, z, one, j with *40  have constant := polynomialConstant.member at I, A, z, leading with *41  have target : IsCommRing(P)42    exact polynomials.comm_ring with *43  have hom : IsRingHom(polynomialCoefficients(I, R), R, P)44    exact polynomialCoefficients.hom with *45  unfold polynomialFromHorner46  exact hornerValue.closed with *4748theorem polynomialFromHorner.cons (c : Set) (cs : List(A))49  requires coefficient : c ∈ R50  shows polynomialFromHorner(I, R, j, leading, c :: cs) = P[polynomialConstant(I, R, c) + polynomialVariable(I, R, j) * polynomialFromHorner(I, R, j, leading, cs)]51proof52  have ordinary := IsCommRing.ring with ring53  have zeroIn := IsRing.zero_in_carrier with ordinary54  have value := polynomialCoefficients.value at I, A, z, c with *55  unfold polynomialFromHorner56  rw [monicValue, value]57  rfl5859section Assignments60variable (v : Set)61hypothesis assignment : v : I → R62hypothesis index : j ∈ I6364theorem polynomialAt.from_horner (cs : List(A))65  shows polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) = hornerAt{A}(add, mul, leading, v(j), cs)66proof67  induction cs68  | List.nil =>69    rw [polynomialFromHorner.nil, hornerAt.nil]70    exact polynomialAt.constant with *71  | List.cons(c, tail) using ih =>72    have coefficient : c ∈ R by assumption73    have ordinary := IsCommRing.ring with ring74    have zeroIn := IsRing.zero_in_carrier with ordinary75    have monoid := IsRing.multiplicative with ordinary76    have oneIn := IsMonoid.unit_in_carrier with monoid77    have source : IsCommRing(P)78      exact polynomials.comm_ring with *79    have polynomialRing := IsCommRing.ring with source80    have constant := polynomialConstant.member at I, A, z, c with *81    have variable := polynomialVariable.member at I, A, z, one, j with *82    have tailMember : polynomialFromHorner(I, R, j, leading, tail) ∈ P83      exact polynomialFromHorner.member with *84    have product := IsRing.mul_closed with polynomialRing, variable, tailMember85    have evaluation : IsRingHom(polynomialAt(I, R, v), P, R)86      exact polynomialAt.hom with *87    have sumValue := IsRingHom.add with evaluation, constant, product88    have productValue := IsRingHom.mul with evaluation, variable, tailMember89    have constantValue := polynomialAt.constant with coefficient90    have variableValue := polynomialAt.variable with *91    rw [polynomialFromHorner.cons, hornerAt.cons]92    cc9394end Assignments95end Rings9697section Fields98variable (I A add z neg mul one j leading : Set)99notation ring R := (A, add, z, neg, mul, one)100notation ring P := R[I]101hypothesis field : IsField(R)102hypothesis initial : leading ∈ R103hypothesis nonzero : leading ≠ R[0]104hypothesis infinite : ¬Finite(R)105hypothesis index : j ∈ I106107theorem polynomialFromHorner.nonvanishing (cs : List(A))108  shows ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) ≠ R[0]109proof110  have point : ∃ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]111    exact hornerAt.exists_nonzero with *112  obtain ⟨x, element, value⟩ := point113  have ring := IsField.comm_ring with field114  have assignment := constantFunction.function at I, A, x with element115  have coordinate := constantFunction.apply at I, A, j, x with *116  have evaluation := polynomialAt.from_horner at I, A, add, z, neg, mul, one, j, leading, constantFunction(I, A, x), cs with *117  refine ⟨constantFunction(I, A, x), assignment, ?_⟩118  rwa [evaluation, coordinate]119120theorem polynomialFromHorner.nonzero (cs : List(A))121  shows polynomialFromHorner(I, R, j, leading, cs) ≠ P[0]122proof123  have ring := IsField.comm_ring with field124  have point : ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) ≠ R[0]125    exact polynomialFromHorner.nonvanishing with *126  obtain ⟨v, assignment, nonvanishing⟩ := point127  have evaluation : IsRingHom(polynomialAt(I, R, v), P, R)128    exact polynomialAt.hom with *129  have zeroValue := IsRingHom.zero with evaluation130  intro equal131  apply nonvanishing132  rwa equal133134end Fields135