Grace/Cumulus/Algebra/Polynomial/VariableCoefficients.g17

Imports

Declarations

Source

1-- Coefficients in one variable, as sparse polynomials in the remaining variables (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.VariableCoefficients8import Variables9import MonomialGeneration1011defgraph monomialErasure (I j : Set) (m ∈ monomials(I)) : monomials(I) := coefficientErase(I, ℕ, 0, m, j)12proof13  exact monomialErase.member with *1415theorem monomialErase.fixed (I m j : Set)16  requires member : m ∈ monomials(I)17  requires absent : m(j) = 018  shows coefficientErase(I, ℕ, 0, m, j) = m19proof20  have zeroIn := nat.omega.forward with Naturals.constructor.zero21  have function := monomials.function with member22  have erased := coefficientErase.function at I, ℕ, 0, m, j with *23  apply FunctionBetween.ext with erased, function24  intros i hi25  have alternatives : i = j ∨ i ≠ j by tauto26  cases alternatives with same | different27  . rw same28    have index : j ∈ I by cc29    have value := coefficientErase.same with zeroIn, function, index30    cc31  . exact coefficientErase.other with *3233theorem monomialErase.insert (I m j : Set, n : Nat)34  requires member : m ∈ monomials(I)35  requires absent : m(j) = 036  shows coefficientErase(I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j) = m37proof38  have zeroIn := nat.omega.forward with Naturals.constructor.zero39  have nIn := nat.omega.forward at n with *40  have single := monomialSingle.member at I, j, n with *41  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *42  have function := monomials.function with product43  have erased := coefficientErase.function at I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j with *44  have original := monomials.function with member45  apply FunctionBetween.ext with erased, original46  intros i hi47  have alternatives : i = j ∨ i ≠ j by tauto48  cases alternatives with same | different49  . rw same50    have index : j ∈ I by cc51    have value := coefficientErase.same at I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j with *52    cc53  . have value := coefficientErase.other at I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j, i with *54    have productValue := monomialProduct.value at I, coefficientSingle(I, ℕ, 0, n, j), m, i with *55    have singleValue := coefficientSingle.other at I, ℕ, 0, n, j, i with *56    have natural := monomials.exponent at I, m, i with *57    rw [value, productValue, singleValue]58    exact add.left_unit at m(i) with *5960-- At a monomial with zero j-exponent, read the coefficient after inserting n copies of j.61-- At every other monomial the result is zero, so the coefficient polynomial omits j.62defgraph polynomialVariableCoefficient (I A z p j : Set, n : Nat) (m ∈ monomials(I)) : A :=63  singleValue(A, z, p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)), 0, m(j))64requires zeroIn : z ∈ A65requires polynomial : p ∈ polynomials(I, A, z)66proof67  have single := monomialSingle.member at I, j, n with *68  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *69  have coefficient := polynomials.coefficient at I, A, z, p, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *70  exact singleValue.closed with *7172notation scoped polynomialVariableCoefficient(I, R, p, j, n) => polynomialVariableCoefficient(I, R.carrier, R.zero, p, j, n)7374section Coefficients75variable (I A z p j : Set)76hypothesis zeroIn : z ∈ A77hypothesis polynomial : p ∈ polynomials(I, A, z)7879theorem polynomialVariableCoefficient.at_zero (n : Nat, m : Set)80  requires member : m ∈ monomials(I)81  requires absent : m(j) = 082  shows polynomialVariableCoefficient(I, A, z, p, j, n)(m) = p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m))83proof84  have single := monomialSingle.member at I, j, n with *85  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *86  have coefficient := polynomials.coefficient at I, A, z, p, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *87  have value := polynomialVariableCoefficient.value at I, A, z, p, j, n, m with *88  have selected := singleValue.same at A, z, p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)), 0, m(j) with *89  cc9091theorem polynomialVariableCoefficient.at_nonzero (n : Nat, m : Set)92  requires member : m ∈ monomials(I)93  requires present : m(j) ≠ 094  shows polynomialVariableCoefficient(I, A, z, p, j, n)(m) = z95proof96  have single := monomialSingle.member at I, j, n with *97  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *98  have coefficient := polynomials.coefficient at I, A, z, p, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *99  have value := polynomialVariableCoefficient.value at I, A, z, p, j, n, m with *100  have selected := singleValue.other at A, z, p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)), 0, m(j) with *101  cc102103theorem polynomialVariableCoefficient.support (n : Nat)104  shows functionSupport(polynomialVariableCoefficient(I, A, z, p, j, n), monomials(I), z) ⊆ functionImage(monomialErasure(I, j), functionSupport(p, monomials(I), z), monomials(I))105proof106  intros m hm107  have data := functionSupport.membership.forward with hm108  have absent : m(j) = 0109    by_contra present110    have vanishes := polynomialVariableCoefficient.at_nonzero at I, A, z, p, j, n, m with *111    exact data.right with vanishes112  have single := monomialSingle.member at I, j, n with *113  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *114  have value := polynomialVariableCoefficient.at_zero at I, A, z, p, j, n, m with *115  have nonzero : p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)) ≠ z116    rw ← value117    exact data.right118  have supported : monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) ∈ functionSupport(p, monomials(I), z)119    exact functionSupport.membership.backward with ⟨product, nonzero⟩120  have erased := monomialErase.insert at I, m, j, n with *121  have imageValue := monomialErasure.value at I, j, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *122  apply functionImage.membership.backward123  refine ⟨data.left, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), supported, ?_⟩124  cc125126theorem polynomialVariableCoefficient.member (n : Nat)127  shows polynomialVariableCoefficient(I, A, z, p, j, n) ∈ polynomials(I, A, z)128proof129  have function := polynomialVariableCoefficient.function at I, A, z, p, j, n with *130  have support := polynomialVariableCoefficient.support at I, A, z, p, j, n with *131  have finite := polynomials.finite_support with polynomial132  have domain := functionSupport.subset at p, monomials(I), z133  have erasure := monomialErasure.function at I, j134  have imageFinite := Finite.function_image with erasure, finite, domain135  have finiteSupport := Finite.subset with imageFinite, support136  apply polynomials.contains137  unfold CoefficientMap138  refine ⟨function, finiteSupport⟩139140theorem polynomialVariableCoefficient.recover (m : Set)141  requires member : m ∈ monomials(I)142  requires index : j ∈ I143  shows polynomialVariableCoefficient(I, A, z, p, j, m(j))(coefficientErase(I, ℕ, 0, m, j)) = p(m)144proof145  have naturalZero := nat.omega.forward with Naturals.constructor.zero146  have function := monomials.function with member147  have exponent := monomials.exponent at I, m, j with *148  have erased := monomialErase.member at I, m, j with *149  have absent := coefficientErase.same at I, ℕ, 0, m, j with *150  have value := polynomialVariableCoefficient.at_zero at I, A, z, p, j, m(j), coefficientErase(I, ℕ, 0, m, j) with *151  have restore := monomialErase.restore at I, m, j with *152  cc153154theorem polynomialVariableCoefficient.variables (n : Nat)155  shows polynomialVariablesUsed(I, A, z, polynomialVariableCoefficient(I, A, z, p, j, n)) ⊆ polynomialVariablesUsed(I, A, z, p) ∖ {j}156proof157  have bound := polynomialVariableCoefficient.support at I, A, z, p, j, n with *158  intros i hi159  obtain ⟨m, support, used⟩ := polynomialVariablesUsed.membership.forward with hi160  have image := bound with m, support161  obtain ⟨member, t, supported, equal⟩ := functionImage.membership.forward with image162  have data := functionSupport.membership.forward with supported163  have value := monomialErasure.value at I, j, t with data.left164  have same : m = coefficientErase(I, ℕ, 0, t, j) by cc165  have naturalZero := nat.omega.forward with Naturals.constructor.zero166  have function := monomials.function with data.left167  have erasedSupport := coefficientErase.support at I, ℕ, 0, t, j with *168  rw same at used169  have inDifference := erasedSupport with i, used170  have old := difference.membership.forward with inDifference171  have original : i ∈ polynomialVariablesUsed(I, A, z, p)172    exact polynomialVariablesUsed.membership.backward with ⟨t, supported, old.left⟩173  exact difference.membership.backward with ⟨original, old.right⟩174175theorem polynomialVariableCoefficient.ext (q : Set)176  requires other : q ∈ polynomials(I, A, z)177  requires index : j ∈ I178  requires coefficients : ∀ n ∈ ℕ, polynomialVariableCoefficient(I, A, z, p, j, n) = polynomialVariableCoefficient(I, A, z, q, j, n)179  shows p = q180proof181  apply polynomials.ext with polynomial, other182  intros m hm183  have exponent := monomials.exponent with *184  have exponentIn := nat.omega.forward at m(j) with *185  have equal := coefficients with m(j), exponentIn186  have left := polynomialVariableCoefficient.recover at I, A, z, p, j, m with *187  have right := polynomialVariableCoefficient.recover at I, A, z, q, j, m with *188  cc189190theorem polynomialVariableCoefficient.exists_nonzero191  requires index : j ∈ I192  requires nonzero : p ≠ constantFunction(monomials(I), A, z)193  shows ∃ n ∈ ℕ, polynomialVariableCoefficient(I, A, z, p, j, n) ≠ constantFunction(monomials(I), A, z)194proof195  by_contra none196  apply nonzero197  have function := polynomials.function with polynomial198  have zeroFunction := constantFunction.function at monomials(I), A, z with *199  apply FunctionBetween.ext with function, zeroFunction200  intros m hm201  have exponent := monomials.exponent with *202  have exponentIn := nat.omega.forward at m(j) with *203  have equal : polynomialVariableCoefficient(I, A, z, p, j, m(j)) = constantFunction(monomials(I), A, z)204    by_contra different205    apply none206    refine ⟨m(j), exponentIn, different⟩207  have erased := monomialErase.member at I, m, j with *208  have recovery := polynomialVariableCoefficient.recover at I, A, z, p, j, m with *209  have erasedZero := constantFunction.apply at monomials(I), A, coefficientErase(I, ℕ, 0, m, j), z with *210  have originalZero := constantFunction.apply at monomials(I), A, m, z with *211  cc212213end Coefficients214