Grace/Cumulus/Algebra/Polynomial/ConvolutionLaws.g17
Imports
Convolution · Ring.PushforwardTransport
Declarations
Source
1-- Algebraic laws for the constructed finite convolution (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.ConvolutionLaws8import Convolution9import Ring.PushforwardTransport1011theorem polynomialProduct.commutative (I A add zero neg mul one p q : Set)12 requires ring : IsCommRing(A, add, zero, neg, mul, one)13 requires memberP : p ∈ polynomials(I, A, zero)14 requires memberQ : q ∈ polynomials(I, A, zero)15 shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) = polynomialProduct(I, A, add, zero, neg, mul, one, q, p)16proof17 have finite := convolutionPairs.finite at I, A, zero, p, q with *18 have weightsPQ := convolutionWeights.function at I, A, add, zero, neg, mul, one, p, q with *19 have weightsQP := convolutionWeights.function at I, A, add, zero, neg, mul, one, q, p with *20 have swap : BijectiveBetween(productSwap(functionSupport(p, monomials(I), zero), functionSupport(q, monomials(I), zero)), convolutionPairs(I, zero, p, q), convolutionPairs(I, zero, q, p))21 unfold convolutionPairs22 exact productSwap.bijective23 have indices : ∀ t ∈ convolutionPairs(I, zero, p, q), monomialMul(I)(t) = monomialMul(I)(productSwap(functionSupport(p, monomials(I), zero), functionSupport(q, monomials(I), zero))(t))24 intros t ht25 unfold convolutionPairs at ht26 obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht27 have dataU := functionSupport.membership.forward with hu28 have dataV := functionSupport.membership.forward with hv29 have swapped := productSwap.pair with hu, hv30 have first := monomialMul.apply at I, u, v with *31 have second := monomialMul.apply at I, v, u with *32 have comm := monomialProduct.commutative at I, u, v with *33 unfold call2 at first34 unfold call2 at second35 cc36 have weights : ∀ t ∈ convolutionPairs(I, zero, p, q), convolutionWeights(I, A, add, zero, neg, mul, one, p, q)(t) = convolutionWeights(I, A, add, zero, neg, mul, one, q, p)(productSwap(functionSupport(p, monomials(I), zero), functionSupport(q, monomials(I), zero))(t))37 intros t ht38 unfold convolutionPairs at ht39 obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht40 have dataU := functionSupport.membership.forward with hu41 have dataV := functionSupport.membership.forward with hv42 have coefficientP := polynomials.coefficient at I, A, zero, p, u with *43 have coefficientQ := polynomials.coefficient at I, A, zero, q, v with *44 have swapped := productSwap.pair with hu, hv45 have first := convolutionWeights.pair with hu, hv46 have second := convolutionWeights.pair with hv, hu47 have comm : call2(mul, p(u), q(v)) = call2(mul, q(v), p(u)) by ring48 cc49 unfold polynomialProduct50 exact finitePushforward.reindex with *51