Grace/Cumulus/Algebra/Polynomial/ConvolutionBounds.g17

Open in Workbench Download source

Imports

ConvolutionLaws

Declarations

Source

1-- Convolution over arbitrary finite bounds containing every support pair (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.ConvolutionBounds8import ConvolutionLaws910theorem polynomialPairCoefficient.pair (I A add zero neg mul one p q u v : 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 monomialU : u ∈ monomials(I)15  requires monomialV : v ∈ monomials(I)16  shows polynomialPairCoefficient(I, A, add, zero, neg, mul, one, p, q, (u, v)) = call2(mul, p(u), q(v))17proof18  have pair := product.pair at u, v, monomials(I), monomials(I) with *19  have selected := polynomialPairCoefficient.selected at I, A, add, zero, neg, mul, one, p, q, (u, v) with *20  obtain ⟨a, ha, b, hb, shape, output⟩ := selected.right21  have coordinates := orderedPair.injective with shape22  cc2324defgraph boundedConvolutionWeights (I D A add zero neg mul one p q : Set) (t ∈ D) : A :=25  polynomialPairCoefficient(I, A, add, zero, neg, mul, one, p, q, t)26requires ring : IsCommRing(A, add, zero, neg, mul, one)27requires memberP : p ∈ polynomials(I, A, zero)28requires memberQ : q ∈ polynomials(I, A, zero)29requires domain : D ⊆ monomials(I) × monomials(I)30proof31  have pair := domain with t, member32  have selected := polynomialPairCoefficient.selected at I, A, add, zero, neg, mul, one, p, q, t with *33  exact selected.left3435section Bounds36variable (I D A add zero neg mul one p q : Set)37hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)38hypothesis memberP : p ∈ polynomials(I, A, zero)39hypothesis memberQ : q ∈ polynomials(I, A, zero)40hypothesis domain : D ⊆ monomials(I) × monomials(I)41notation ring R := (A, add, zero, neg, mul, one)4243theorem boundedConvolutionWeights.pair (u v : Set)44  requires pair : (u, v) ∈ D45  requires monomialU : u ∈ monomials(I)46  requires monomialV : v ∈ monomials(I)47  shows boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q)((u, v)) = p(u) * q(v)48proof49  have value := boundedConvolutionWeights.value at I, D, A, add, zero, neg, mul, one, p, q, (u, v) with *50  have coefficient := polynomialPairCoefficient.pair at I, A, add, zero, neg, mul, one, p, q, u, v with *51  cc5253theorem boundedConvolutionWeights.outside (t : Set)54  requires pair : t ∈ D55  requires outside : ¬(t ∈ convolutionPairs(I, zero, p, q))56  shows boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q)(t) = zero57proof58  have included := domain59  have inProduct := included with t, pair60  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with inProduct61  have inD : (u, v) ∈ D by rwa ← shape62  have coefficientP := polynomials.coefficient at I, A, zero, p, u with *63  have coefficientQ := polynomials.coefficient at I, A, zero, q, v with *64  have value := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, q, u, v with *65  have alternatives : u ∈ functionSupport(p, monomials(I), zero) ∨ ¬(u ∈ functionSupport(p, monomials(I), zero))66    tauto67  have productZero : p(u) * q(v) = 068    cases alternatives with supportP | absentP69    . have absentQ : ¬(v ∈ functionSupport(q, monomials(I), zero))70        intro supportQ71        have pairIn := product.pair with supportP, supportQ72        have supported : t ∈ convolutionPairs(I, zero, p, q)73          unfold convolutionPairs74          rwa shape75        exact outside with supported76      have vanishes := functionSupport.outside with *77      rw vanishes78      ring79    . have vanishes := functionSupport.outside with *80      rw vanishes81      ring82  cc8384theorem polynomialProduct.on_domain85  requires finite : Finite(D)86  requires covers : convolutionPairs(I, zero, p, q) ⊆ D87  shows finitePushforward(D, monomials(I), A, add, zero, neg, mul, one, monomialMul(I), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q)) = polynomialProduct(I, A, add, zero, neg, mul, one, p, q)88proof89  have weights := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, q with *90  have original := convolutionWeights.function at I, A, add, zero, neg, mul, one, p, q with *91  have agreement : ∀ t ∈ convolutionPairs(I, zero, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q)(t) = convolutionWeights(I, A, add, zero, neg, mul, one, p, q)(t)92    intros t ht93    have included := covers94    have inD := included with t, ht95    have left := boundedConvolutionWeights.value at I, D, A, add, zero, neg, mul, one, p, q, t with *96    have right := convolutionWeights.value at I, A, add, zero, neg, mul, one, p, q, t with *97    cc98  have vanishes : ∀ t ∈ D, ¬(t ∈ convolutionPairs(I, zero, p, q)) → boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q)(t) = zero99    intros t ht outside100    exact boundedConvolutionWeights.outside with *101  have extended := finitePushforward.zero_extension at D, convolutionPairs(I, zero, p, q), monomials(I), A, add, zero, neg, mul, one, monomialMul(I), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), convolutionWeights(I, A, add, zero, neg, mul, one, p, q) with *102  unfold polynomialProduct103  cc104105end Bounds106