Grace/Cumulus/Algebra/Polynomial/Distributivity.g17

Open in Workbench Download source

Imports

ConvolutionBounds

Declarations

Source

1-- Distributivity of finite polynomial convolution via common support bounds (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.Distributivity8import ConvolutionBounds910theorem boundedConvolutionWeights.add (I D A add zero neg mul one p q r : Set)11  requires ring : IsCommRing(A, add, zero, neg, mul, one)12  requires memberP : p ∈ polynomials(I, A, zero)13  requires memberQ : q ∈ polynomials(I, A, zero)14  requires memberR : r ∈ polynomials(I, A, zero)15  requires domain : D ⊆ monomials(I) × monomials(I)16  shows boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) =17    coefficientAdd(D, A, add, zero, neg, mul, one, boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, r))18proof19  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *20  have functionQ := polynomials.function with memberQ21  have functionR := polynomials.function with memberR22  have leftFunction := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *23  have weightsQ := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, q with *24  have weightsR := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, r with *25  have rightFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, r) with *26  apply FunctionBetween.ext with leftFunction, rightFunction27  intros t ht28  have included := domain29  have pair := included with t, ht30  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with pair31  have inD : (u, v) ∈ D by rwa ← shape32  have pValue := polynomials.coefficient at I, A, zero, p, u with *33  have qValue := polynomials.coefficient at I, A, zero, q, v with *34  have rValue := polynomials.coefficient at I, A, zero, r, v with *35  have sumValue := coefficientAdd.value at monomials(I), A, add, zero, neg, mul, one, q, r, v with *36  have left := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r), u, v with *37  have first := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, q, u, v with *38  have second := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, r, u, v with *39  have right := coefficientAdd.value at D, A, add, zero, neg, mul, one, boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, r), (u, v) with *40  have distribute : call2(mul, p(u), call2(add, q(v), r(v))) = call2(add, call2(mul, p(u), q(v)), call2(mul, p(u), r(v)))41    ring42  cc4344theorem convolutionPairs.add_subset (I A add zero neg mul one p q r : Set)45  requires ring : IsCommRing(A, add, zero, neg, mul, one)46  requires memberQ : q ∈ polynomials(I, A, zero)47  requires memberR : r ∈ polynomials(I, A, zero)48  shows convolutionPairs(I, zero, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) ⊆ convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r)49proof50  have functionQ := polynomials.function with memberQ51  have functionR := polynomials.function with memberR52  have support := coefficientAdd.support at monomials(I), A, add, zero, neg, mul, one, q, r with *53  intros t ht54  unfold convolutionPairs at ht55  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht56  have inUnion := support with v, hv57  have alternatives := union2.membership.forward with inUnion58  apply union2.membership.backward59  cases alternatives with inQ | inR60  . left61    unfold convolutionPairs62    rw shape63    exact product.pair with hu, inQ64  . right65    unfold convolutionPairs66    rw shape67    exact product.pair with hu, inR6869theorem polynomialProduct.add_right (I A add zero neg mul one p q r : Set)70  requires ring : IsCommRing(A, add, zero, neg, mul, one)71  requires memberP : p ∈ polynomials(I, A, zero)72  requires memberQ : q ∈ polynomials(I, A, zero)73  requires memberR : r ∈ polynomials(I, A, zero)74  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) =75    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))76proof77  have finiteQ := convolutionPairs.finite with memberP, memberQ78  have finiteR := convolutionPairs.finite with memberP, memberR79  have finite := Finite.union with finiteQ, finiteR80  have domainQ := convolutionPairs.subset at I, zero, p, q81  have domainR := convolutionPairs.subset at I, zero, p, r82  have domain : convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r) ⊆ monomials(I) × monomials(I)83    simp [Subset, union2.membership]84  have coversQ : convolutionPairs(I, zero, p, q) ⊆ convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r)85    simp [Subset, union2.membership]86  have coversR : convolutionPairs(I, zero, p, r) ⊆ convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r)87    simp [Subset, union2.membership]88  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *89  have coversSum := convolutionPairs.add_subset at I, A, add, zero, neg, mul, one, p, q, r with *90  have boundQ := polynomialProduct.on_domain with ring, memberP, memberQ, domain, finite, coversQ91  have boundR := polynomialProduct.on_domain with ring, memberP, memberR, domain, finite, coversR92  have boundSum := polynomialProduct.on_domain with ring, memberP, memberSum, domain, finite, coversSum93  have weightSum := boundedConvolutionWeights.add with ring, memberP, memberQ, memberR, domain94  have weightsQ := boundedConvolutionWeights.function at I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, q with *95  have weightsR := boundedConvolutionWeights.function at I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, r with *96  have distribute := finitePushforward.add at A, add, zero, neg, mul, one, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), monomials(I), monomialMul(I), boundedConvolutionWeights(I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, r) with *97  cc9899theorem polynomialProduct.add_left (I A add zero neg mul one p q r : Set)100  requires ring : IsCommRing(A, add, zero, neg, mul, one)101  requires memberP : p ∈ polynomials(I, A, zero)102  requires memberQ : q ∈ polynomials(I, A, zero)103  requires memberR : r ∈ polynomials(I, A, zero)104  shows polynomialProduct(I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r) =105    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))106proof107  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *108  have exchange := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *109  have distribute := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, r, p, q with *110  have first := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, r, p with *111  have second := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, r, q with *112  cc113