Grace/Cumulus/Algebra/Polynomial/VariableExpansion.g17

Open in Workbench Download source

Imports

VariableCoefficients

Declarations

Source

1-- A sparse polynomial has only finitely many nonzero coefficients in any one variable.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.VariableExpansion8import VariableCoefficients910defgraph monomialExponent (I j : Set) (m ∈ monomials(I)) : ℕ := m(j)11requires index : j ∈ I12proof13  have natural := monomials.exponent at I, m, j with *14  exact nat.omega.forward at m(j) with *1516defgraph polynomialCoefficientFamily (I A z p j : Set) (n ∈ ℕ) : polynomials(I, A, z) := polynomialVariableCoefficient(I, A, z, p, j, n)17requires zeroIn : z ∈ A18requires polynomial : p ∈ polynomials(I, A, z)19proof20  have natural := nat.omega.backward at n with *21  exact polynomialVariableCoefficient.member with *2223notation scoped polynomialCoefficientFamily(I, R, p, j) => polynomialCoefficientFamily(I, R.carrier, R.zero, p, j)2425section Expansion26variable (I A z p j : Set)27hypothesis zeroIn : z ∈ A28hypothesis polynomial : p ∈ polynomials(I, A, z)29hypothesis index : j ∈ I3031theorem polynomialVariableCoefficient.outside (n : Nat)32  requires absent : ¬(n ∈ functionImage(monomialExponent(I, j), functionSupport(p, monomials(I), z), ℕ))33  shows polynomialVariableCoefficient(I, A, z, p, j, n) = constantFunction(monomials(I), A, z)34proof35  have function := polynomialVariableCoefficient.function at I, A, z, p, j, n with *36  have zeroFunction := constantFunction.function at monomials(I), A, z with *37  apply FunctionBetween.ext with function, zeroFunction38  intros m hm39  have zeroValue := constantFunction.apply at monomials(I), A, m, z with *40  rw zeroValue41  have alternatives : m(j) = 0 ∨ m(j) ≠ 0 by tauto42  cases alternatives with missing | present43  . have value := polynomialVariableCoefficient.at_zero with *44    rw value45    by_contra nonzero46    have naturalZero := nat.omega.forward with Naturals.constructor.zero47    have nIn := nat.omega.forward at n with *48    have single := monomialSingle.member at I, j, n with *49    have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *50    have exponent := monomialProduct.value at I, coefficientSingle(I, ℕ, 0, n, j), m, j with *51    have singleValue := coefficientSingle.same at I, ℕ, 0, n, j with *52    have identity := add.right_unit with *53    have equal : monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)(j) = n by cc54    have imageValue := monomialExponent.value at I, j, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *55    have supported : monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) ∈ functionSupport(p, monomials(I), z)56      exact functionSupport.membership.backward with ⟨product, nonzero⟩57    apply absent58    apply functionImage.membership.backward59    refine ⟨nIn, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), supported, ?_⟩60    cc61  . exact polynomialVariableCoefficient.at_nonzero with *6263theorem polynomialCoefficientFamily.support64  shows functionSupport(polynomialCoefficientFamily(I, A, z, p, j), ℕ, constantFunction(monomials(I), A, z)) ⊆ functionImage(monomialExponent(I, j), functionSupport(p, monomials(I), z), ℕ)65proof66  intros n hn67  have data := functionSupport.membership.forward with hn68  have natural := nat.omega.backward with data.left69  have value := polynomialCoefficientFamily.value at I, A, z, p, j, n with *70  by_contra absent71  have vanishes := polynomialVariableCoefficient.outside with *72  apply data.right73  cc7475theorem polynomialCoefficientFamily.finite_support76  shows Finite(functionSupport(polynomialCoefficientFamily(I, A, z, p, j), ℕ, constantFunction(monomials(I), A, z)))77proof78  have finite := polynomials.finite_support with polynomial79  have domain := functionSupport.subset at p, monomials(I), z80  have exponents := monomialExponent.function at I, j with *81  have imageFinite := Finite.function_image with exponents, finite, domain82  have bound := polynomialCoefficientFamily.support with *83  exact Finite.subset with imageFinite, bound8485theorem polynomialCoefficientFamily.map86  shows CoefficientMap(polynomialCoefficientFamily(I, A, z, p, j), ℕ, polynomials(I, A, z), constantFunction(monomials(I), A, z))87proof88  have function := polynomialCoefficientFamily.function at I, A, z, p, j with *89  have finite := polynomialCoefficientFamily.finite_support with *90  unfold CoefficientMap91  refine ⟨function, finite⟩9293end Expansion94theorem polynomialVariableCoefficient.agree_away (I A add z neg mul one p j v w : Set, n : Nat)95  requires ring : IsCommRing(A, add, z, neg, mul, one)96  requires polynomial : p ∈ polynomials(I, A, z)97  requires first : v : I → A98  requires second : w : I → A99  requires agreement : ∀ i ∈ I, i ≠ j → v(i) = w(i)100  shows polynomialAt(I, A, add, z, neg, mul, one, v)(polynomialVariableCoefficient(I, A, z, p, j, n)) = polynomialAt(I, A, add, z, neg, mul, one, w)(polynomialVariableCoefficient(I, A, z, p, j, n))101proof102  have ordinary := IsCommRing.ring with ring103  have zeroIn := IsRing.zero_in_carrier with ordinary104  have coefficient := polynomialVariableCoefficient.member at I, A, z, p, j, n with *105  have bound := polynomialVariableCoefficient.variables at I, A, z, p, j, n with *106  have domain := polynomialVariablesUsed.subset at I, A, z, p107  have same : ∀ i ∈ polynomialVariablesUsed(I, A, z, polynomialVariableCoefficient(I, A, z, p, j, n)), v(i) = w(i)108    intros i hi109    have data := bound with i, hi110    have difference := difference.membership.forward with data111    have inI := domain with i, difference.left112    have different : i ≠ j113      intro equal114      have singleton := singleton.membership.backward with equal115      exact difference.right with singleton116    exact agreement with i, inI, different117  exact polynomialAt.agree_on_variables with *118