Grace/Cumulus/Algebra/Polynomial/Convolution.g17

Open in Workbench Download source

Imports

Polynomial · Ring.Pushforward · Cardinal.Product

Declarations

Source

1-- Polynomial multiplication by finite convolution of coefficient supports (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.Convolution8import Polynomial9import Ring.Pushforward10import Cardinal.Product1112def convolutionPairs (I zero p q : Set) : Set :=13  functionSupport(p, monomials(I), zero) × functionSupport(q, monomials(I), zero)1415theorem convolutionPairs.subset (I zero p q : Set)16  shows convolutionPairs(I, zero, p, q) ⊆ monomials(I) × monomials(I)17proof18  have supportP := functionSupport.subset at p, monomials(I), zero19  have supportQ := functionSupport.subset at q, monomials(I), zero20  unfold convolutionPairs21  exact product.monotone with supportP, supportQ2223theorem convolutionPairs.finite (I A zero p q : Set)24  requires memberP : p ∈ polynomials(I, A, zero)25  requires memberQ : q ∈ polynomials(I, A, zero)26  shows Finite(convolutionPairs(I, zero, p, q))27proof28  have finiteP := polynomials.finite_support with memberP29  have finiteQ := polynomials.finite_support with memberQ30  unfold convolutionPairs31  exact Finite.product with finiteP, finiteQ3233defunique polynomialPairCoefficient (I A add zero neg mul one p q t : Set) (a ∈ A) :=34  ∃ m ∈ monomials(I), ∃ n ∈ monomials(I), t = (m, n) ∧ a = call2(mul, p(m), q(n))35requires ring : IsCommRing(A, add, zero, neg, mul, one)36requires memberP : p ∈ polynomials(I, A, zero)37requires memberQ : q ∈ polynomials(I, A, zero)38requires pair : t ∈ monomials(I) × monomials(I)39proof40  obtain ⟨bound, m, hm, n, hn, shape⟩ := product.membership.forward with pair41  have pIn := polynomials.coefficient at I, A, zero, p, m with *42  have qIn := polynomials.coefficient at I, A, zero, q, n with *43  have ordinary := IsCommRing.ring with ring44  have valueIn := IsRing.mul_closed at A, add, zero, neg, mul, one, p(m), q(n) with *45  refine ⟨call2(mul, p(m), q(n)), valueIn, m, hm, n, hn, shape, rfl⟩46uniqueness47  intros u hu first v hv second48  obtain ⟨m, hm, n, hn, shapeU, valueU⟩ := first49  obtain ⟨r, hr, s, hs, shapeV, valueV⟩ := second50  have equalPairs : (m, n) = (r, s) by cc51  have coordinates := orderedPair.injective with equalPairs52  cc5354defgraph convolutionWeights (I A add zero neg mul one p q : Set) (t ∈ convolutionPairs(I, zero, p, q)) : A :=55  polynomialPairCoefficient(I, A, add, zero, neg, mul, one, p, q, t)56requires ring : IsCommRing(A, add, zero, neg, mul, one)57requires memberP : p ∈ polynomials(I, A, zero)58requires memberQ : q ∈ polynomials(I, A, zero)59proof60  have subset := convolutionPairs.subset at I, zero, p, q61  have pair := subset with t, member62  have selected := polynomialPairCoefficient.selected at I, A, add, zero, neg, mul, one, p, q, t with *63  exact selected.left6465def polynomialProduct (I A add zero neg mul one p q : Set) : Set :=66  finitePushforward(convolutionPairs(I, zero, p, q), monomials(I), A, add, zero, neg, mul, one,67    monomialMul(I), convolutionWeights(I, A, add, zero, neg, mul, one, p, q))6869section Rings70variable (I A add zero neg mul one p q : Set)71hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)72hypothesis memberP : p ∈ polynomials(I, A, zero)73hypothesis memberQ : q ∈ polynomials(I, A, zero)74notation ring R := (A, add, zero, neg, mul, one)7576theorem convolutionWeights.pair (m n : Set)77  requires supportM : m ∈ functionSupport(p, monomials(I), zero)78  requires supportN : n ∈ functionSupport(q, monomials(I), zero)79  shows convolutionWeights(I, A, add, zero, neg, mul, one, p, q)((m, n)) = p(m) * q(n)80proof81  have dataM := functionSupport.membership.forward with supportM82  have dataN := functionSupport.membership.forward with supportN83  have pair := product.pair at m, n, monomials(I), monomials(I) with *84  have supported : (m, n) ∈ convolutionPairs(I, zero, p, q)85    unfold convolutionPairs86    exact product.pair with supportM, supportN87  have selected := polynomialPairCoefficient.selected at I, A, add, zero, neg, mul, one, p, q, (m, n) with *88  obtain ⟨r, hr, s, hs, shape, output⟩ := selected.right89  have coordinates := orderedPair.injective with shape90  have value := convolutionWeights.value at I, A, add, zero, neg, mul, one, p, q, (m, n) with *91  cc9293theorem polynomialProduct.member94  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ polynomials(I, A, zero)95proof96  have finite := convolutionPairs.finite with memberP, memberQ97  have weights := convolutionWeights.function at I, A, add, zero, neg, mul, one, p, q with *98  have indexMap := monomialMul.function at I99  have domain := convolutionPairs.subset at I, zero, p, q100  have map := finitePushforward.map with *101  apply polynomials.contains102  unfold polynomialProduct103  exact map104105theorem polynomialProduct.support106  shows functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, q), monomials(I), zero) ⊆107    functionImage(monomialMul(I), convolutionPairs(I, zero, p, q), monomials(I))108proof109  have finite := convolutionPairs.finite with memberP, memberQ110  have weights := convolutionWeights.function at I, A, add, zero, neg, mul, one, p, q with *111  unfold polynomialProduct112  exact finitePushforward.support with *113114theorem polynomialProduct.support_factor (m : Set)115  requires supported : m ∈ functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, q), monomials(I), zero)116  shows ∃ u ∈ functionSupport(p, monomials(I), zero), ∃ v ∈ functionSupport(q, monomials(I), zero), m = monomialProduct(I, u, v)117proof118  have bound := polynomialProduct.support at I, A, add, zero, neg, mul, one, p, q with *119  have image := bound with m, supported120  obtain ⟨monomial, t, ht, equation⟩ := functionImage.membership.forward with image121  unfold convolutionPairs at ht122  obtain ⟨bounded, u, hu, v, hv, shape⟩ := product.membership.forward with ht123  have dataU := functionSupport.membership.forward with hu124  have dataV := functionSupport.membership.forward with hv125  have value := monomialMul.apply at I, u, v with *126  unfold call2 at value127  refine ⟨u, hu, v, hv, _⟩128  cc129130end Rings131132section Zero133variable (I A add zero neg mul one p : Set)134hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)135hypothesis memberP : p ∈ polynomials(I, A, zero)136137theorem polynomialProduct.zero_left138  shows polynomialProduct(I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p) = constantFunction(monomials(I), A, zero)139proof140  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *141  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p with *142  have ordinary := IsCommRing.ring with ring143  have zeroIn := IsRing.zero_in_carrier with ordinary144  apply polynomials.ext with product, zeroPolynomial145  intros m hm146  have zeroValue := constantFunction.apply at monomials(I), A, m, zero with *147  rw zeroValue148  have alternatives : polynomialProduct(I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p)(m) = zero ∨ polynomialProduct(I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p)(m) ≠ zero149    tauto150  cases alternatives with vanishes | nonzero151  . exact vanishes152  . have supported : m ∈ functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p), monomials(I), zero)153      exact functionSupport.membership.backward with ⟨hm, nonzero⟩154    obtain ⟨u, hu, v, hv, equation⟩ := polynomialProduct.support_factor at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p, m with *155    have data := functionSupport.membership.forward with hu156    have value := constantFunction.apply at monomials(I), A, u, zero with *157    exfalso158    exact data.right with value159160theorem polynomialProduct.zero_right161  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero)) = constantFunction(monomials(I), A, zero)162proof163  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *164  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *165  have ordinary := IsCommRing.ring with ring166  have zeroIn := IsRing.zero_in_carrier with ordinary167  apply polynomials.ext with product, zeroPolynomial168  intros m hm169  have zeroValue := constantFunction.apply at monomials(I), A, m, zero with *170  rw zeroValue171  have alternatives : polynomialProduct(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero))(m) = zero ∨ polynomialProduct(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero))(m) ≠ zero172    tauto173  cases alternatives with vanishes | nonzero174  . exact vanishes175  . have supported : m ∈ functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero)), monomials(I), zero)176      exact functionSupport.membership.backward with ⟨hm, nonzero⟩177    obtain ⟨u, hu, v, hv, equation⟩ := polynomialProduct.support_factor at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero), m with *178    have data := functionSupport.membership.forward with hv179    have value := constantFunction.apply at monomials(I), A, v, zero with *180    exfalso181    exact data.right with value182183end Zero184