Grace/Cumulus/Algebra/Polynomial/Evaluation.g17

Open in Workbench Download source

Imports

Origin

Declarations

Source

1-- Linear evaluation of finite-support polynomials from monomial values (ZF).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.Evaluation8import Origin910defgraph polynomialEvaluationWeights (I D A add zero neg mul one h p : Set) (m ∈ D) : A := call2(mul, p(m), h(m))11requires ring : IsCommRing(A, add, zero, neg, mul, one)12requires values : h : monomials(I) → A13requires polynomial : p ∈ polynomials(I, A, zero)14requires domain : D ⊆ monomials(I)15proof16  unfold Subset at domain17  have monomial := domain with m, member18  have coefficient := polynomials.coefficient at I, A, zero, p, m with *19  have image := FunctionBetween.apply_closed at h, monomials(I), A, m with *20  have ordinary := IsCommRing.ring with ring21  exact IsRing.mul_closed at A, add, zero, neg, mul, one, p(m), h(m) with *2223defgraph polynomialEvaluate (I A add zero neg mul one h : Set) (p ∈ polynomials(I, A, zero)) : A :=24  finiteRingSum(functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p))25requires ring : IsCommRing(A, add, zero, neg, mul, one)26requires values : h : monomials(I) → A27proof28  have domain := functionSupport.subset at p, monomials(I), zero29  have finite := polynomials.finite_support with member30  have weights := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p with *31  exact finiteRingSum.closed at functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p) with *3233section Values34variable (I A add zero neg mul one h : Set)35hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)36hypothesis values : h : monomials(I) → A37notation ring R := (A, add, zero, neg, mul, one)3839theorem polynomialEvaluate.on_domain (p D : Set)40  requires polynomial : p ∈ polynomials(I, A, zero)41  requires domain : D ⊆ monomials(I)42  requires finite : Finite(D)43  requires covers : functionSupport(p, monomials(I), zero) ⊆ D44  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) = finiteRingSum(D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p))45proof46  have ordinary := IsCommRing.ring with ring47  have zeroIn := IsRing.zero_in_carrier with ordinary48  have supportDomain := functionSupport.subset at p, monomials(I), zero49  have weights := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, p with *50  have supported := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p with *51  have agreement : ∀ m ∈ functionSupport(p, monomials(I), zero), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p)(m) = polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p)(m)52    intros m hm53    have included := covers54    have inD := included with m, hm55    have left := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, p, m with *56    have right := polynomialEvaluationWeights.value at I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p, m with *57    cc58  have vanishes : ∀ m ∈ D, ¬(m ∈ functionSupport(p, monomials(I), zero)) → polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p)(m) = zero59    intros m hm outside60    have included := domain61    have monomial := included with m, hm62    have image := FunctionBetween.apply_closed at h, monomials(I), A, m with *63    have coefficient := functionSupport.outside at p, monomials(I), zero, m with *64    have weight := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, p, m with *65    rw [weight, coefficient]66    ring67  have extended := finiteRingSum.zero_extension at D, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p) with *68  have value := polynomialEvaluate.value at I, A, add, zero, neg, mul, one, h, p with *69  cc7071theorem polynomialEvaluate.term (a m : Set)72  requires coefficient : a ∈ A73  requires monomial : m ∈ monomials(I)74  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialTerm(I, A, zero, a, m)) = a * h(m)75proof76  have ordinary := IsCommRing.ring with ring77  have zeroIn := IsRing.zero_in_carrier with ordinary78  have polynomial := polynomialTerm.member at I, A, zero, a, m with *79  have covers := polynomialTerm.support at I, A, zero, a, m with *80  have domain : {m} ⊆ monomials(I) by simp [Subset, singleton.membership]81  have finite := Finite.singleton at m82  have member := singleton.self at m83  have bounded := polynomialEvaluate.on_domain with *84  have weights := polynomialEvaluationWeights.function at I, {m}, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m) with *85  have sum := finiteRingSum.singleton with *86  have weight := polynomialEvaluationWeights.value at I, {m}, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m), m with *87  have point := polynomialTerm.same at I, A, zero, a, m with *88  cc8990theorem polynomialEvaluate.zero91  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(constantFunction(monomials(I), A, zero)) = zero92proof93  have ordinary := IsCommRing.ring with ring94  have zeroIn := IsRing.zero_in_carrier with ordinary95  have unit := monomialOne.member at I96  have image := FunctionBetween.apply_closed with *97  have selected := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, zero, monomialOne(I) with *98  have constant := polynomialConstant.zero at I, A, zero with *99  unfold polynomialConstant at constant100  have zeroProduct : zero * h(monomialOne(I)) = zero by ring101  cc102103theorem polynomialEvaluationWeights.add (p q D : Set)104  requires memberP : p ∈ polynomials(I, A, zero)105  requires memberQ : q ∈ polynomials(I, A, zero)106  requires domain : D ⊆ monomials(I)107  shows polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)) = coefficientAdd(D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, q))108proof109  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *110  have functionP := polynomials.function with memberP111  have functionQ := polynomials.function with memberQ112  have weightsP := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, p with *113  have weightsQ := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, q with *114  have leftFunction := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) with *115  have rightFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, q) with *116  apply FunctionBetween.ext with leftFunction, rightFunction117  intros m hm118  have included := domain119  have monomial := included with m, hm120  have coefficientP := polynomials.coefficient at I, A, zero, p, m with *121  have coefficientQ := polynomials.coefficient at I, A, zero, q, m with *122  have image := FunctionBetween.apply_closed at h, monomials(I), A, m with *123  have source := coefficientAdd.value at monomials(I), A, add, zero, neg, mul, one, p, q, m with *124  have left := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), m with *125  have first := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, p, m with *126  have second := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, q, m with *127  have right := coefficientAdd.value at D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, q), m with *128  have distribute : (p(m) + q(m)) * h(m) = p(m) * h(m) + q(m) * h(m) by ring129  cc130131theorem polynomialEvaluate.add (p q : Set)132  requires memberP : p ∈ polynomials(I, A, zero)133  requires memberQ : q ∈ polynomials(I, A, zero)134  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)135proof136  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *137  have functionP := polynomials.function with memberP138  have functionQ := polynomials.function with memberQ139  have finiteP := polynomials.finite_support with memberP140  have finiteQ := polynomials.finite_support with memberQ141  have finite := Finite.union with finiteP, finiteQ142  have domainP := functionSupport.subset at p, monomials(I), zero143  have domainQ := functionSupport.subset at q, monomials(I), zero144  have domain : functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero) ⊆ monomials(I)145    simp [Subset, union2.membership]146  have coversP : functionSupport(p, monomials(I), zero) ⊆ functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero)147    simp [Subset, union2.membership]148  have coversQ : functionSupport(q, monomials(I), zero) ⊆ functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero)149    simp [Subset, union2.membership]150  have coversSum := coefficientAdd.support at monomials(I), A, add, zero, neg, mul, one, p, q with *151  have sumValue := polynomialEvaluate.on_domain with ring, values, memberSum, domain, finite, coversSum152  have firstValue := polynomialEvaluate.on_domain with ring, values, memberP, domain, finite, coversP153  have secondValue := polynomialEvaluate.on_domain with ring, values, memberQ, domain, finite, coversQ154  have weightsP := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, p with *155  have weightsQ := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, q with *156  have weightsSum := polynomialEvaluationWeights.add at I, A, add, zero, neg, mul, one, h, p, q, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero) with *157  have distribute := finiteRingSum.add at functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, q) with *158  cc159160theorem polynomialEvaluate.in_carrier (p : Set)161  requires polynomial : p ∈ polynomials(I, A, zero)162  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) ∈ A163proof164  have function := polynomialEvaluate.function at I, A, add, zero, neg, mul, one, h with *165  exact FunctionBetween.apply_closed with function, polynomial166167theorem polynomialEvaluate.neg (p : Set)168  requires polynomial : p ∈ polynomials(I, A, zero)169  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)) = -polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p)170proof171  have negative := polynomials.neg with *172  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *173  have valueNeg := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *174  have functionP := polynomials.function with polynomial175  have inverse := coefficientAdd.inverse at monomials(I), A, add, zero, neg, mul, one, p with *176  have sum := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, p, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *177  have zeroValue := polynomialEvaluate.zero at I, A, add, zero, neg, mul, one, h with *178  have equation : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)) = zero179    cc180  linear_combination equation181182end Values183