ConvolutionDistributivity

Two-stage grouping and distributivity of polynomial convolution (ZF)

Open in Workbench View on GitHub

1-- Two-stage grouping and distributivity of polynomial 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 ConvolutionDistributivity8import Grace.Cumulus.Algebra.Polynomial.Distributivity910section Rings11variable (A add zero neg mul one : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)1314theorem two_stage_grouping (D C B h k w : Set)15  requires finiteD : Finite(D)16  requires finiteC : Finite(C)17  requires weights : w : D → A18  requires firstMap : h : D → C19  requires secondMap : k : C → B20  shows finitePushforward(C, B, A, add, zero, neg, mul, one, k, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)) =21    finitePushforward(D, B, A, add, zero, neg, mul, one, compose(k, h, D, C, B), w)22proof23  exact finitePushforward.compose with ring, finiteD, weights, firstMap, secondMap, finiteC2425theorem singleton_groups (D w : Set)26  requires finite : Finite(D)27  requires weights : w : D → A28  shows finitePushforward(D, D, A, add, zero, neg, mul, one, identity(D), w) = w29proof30  exact finitePushforward.identity with ring, finite, weights3132theorem distribute_right (I p q r : Set)33  requires memberP : p ∈ polynomials(I, A, zero)34  requires memberQ : q ∈ polynomials(I, A, zero)35  requires memberR : r ∈ polynomials(I, A, zero)36  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) =37    coefficientAdd(monomials(I), A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r))38proof39  exact polynomialProduct.add_right with ring, memberP, memberQ, memberR4041theorem distribute_left (I p q r : Set)42  requires memberP : p ∈ polynomials(I, A, zero)43  requires memberQ : q ∈ polynomials(I, A, zero)44  requires memberR : r ∈ polynomials(I, A, zero)45  shows polynomialProduct(I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r) =46    coefficientAdd(monomials(I), A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, r))47proof48  exact polynomialProduct.add_left with ring, memberP, memberQ, memberR4950end Rings51