Grace/Cumulus/Algebra/Polynomial/Variables.g17

Open in Workbench Download source

Imports

Assignment · Cardinal.FiniteUnion · Cardinal.FiniteImage

Declarations

Source

1-- The finite set of variables used by a sparse polynomial determines its evaluation.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.Variables8import Assignment9import Cardinal.FiniteUnion10import Cardinal.FiniteImage1112defgraph monomialVariableSets (I : Set) (m ∈ monomials(I)) : 𝒫(I) := functionSupport(m, I, 0)13proof14  have subset := functionSupport.subset at m, I, 015  exact powerset.membership_iff.backward at functionSupport(m, I, 0), I with subset1617def polynomialVariablesUsed (I A z p : Set) : Set :=18  ⋃functionImage(monomialVariableSets(I), functionSupport(p, monomials(I), z), 𝒫(I))1920notation scoped polynomialVariablesUsed(I, R, p) => polynomialVariablesUsed(I, R.carrier, R.zero, p)2122theorem polynomialVariablesUsed.membership (I A z p i : Set)23  shows i ∈ polynomialVariablesUsed(I, A, z, p) ↔ ∃ m ∈ functionSupport(p, monomials(I), z), i ∈ functionSupport(m, I, 0)24proof25  constructor26  . intro member27    unfold polynomialVariablesUsed at member28    obtain ⟨S, image, inS⟩ := set.union.forward with member29    obtain ⟨bound, m, support, equal⟩ := functionImage.membership.forward with image30    have data := functionSupport.membership.forward with support31    have value := monomialVariableSets.value with data.left32    refine ⟨m, support, ?_⟩33    have same : S = functionSupport(m, I, 0) by cc34    rwa ← same35  . intro witnesses36    obtain ⟨m, support, member⟩ := witnesses37    have data := functionSupport.membership.forward with support38    have function := monomialVariableSets.function at I39    have bounded := FunctionBetween.apply_closed with function, data.left40    have value := monomialVariableSets.value with data.left41    have image : monomialVariableSets(I)(m) ∈ functionImage(monomialVariableSets(I), functionSupport(p, monomials(I), z), 𝒫(I))42      exact functionImage.membership.backward with ⟨bounded, m, support, rfl⟩43    have inS : i ∈ monomialVariableSets(I)(m) by rwa value44    unfold polynomialVariablesUsed45    exact union.contains with image, inS4647theorem polynomialVariablesUsed.subset (I A z p : Set)48  shows polynomialVariablesUsed(I, A, z, p) ⊆ I49proof50  intros i hi51  obtain ⟨m, support, member⟩ := polynomialVariablesUsed.membership.forward with hi52  have data := functionSupport.membership.forward with member53  exact data.left5455theorem polynomialVariablesUsed.finite (I A z p : Set)56  requires polynomial : p ∈ polynomials(I, A, z)57  shows Finite(polynomialVariablesUsed(I, A, z, p))58proof59  have support := polynomials.finite_support with polynomial60  have domain := functionSupport.subset at p, monomials(I), z61  have function := monomialVariableSets.function at I62  have finite := Finite.function_image with function, support, domain63  have members : ∀ S ∈ functionImage(monomialVariableSets(I), functionSupport(p, monomials(I), z), 𝒫(I)), Finite(S)64    intros S hS65    obtain ⟨bound, m, hm, equal⟩ := functionImage.membership.forward with hS66    have data := functionSupport.membership.forward with hm67    have map := monomials.map with data.left68    have finiteSupport := CoefficientMap.finite_support with map69    have value := monomialVariableSets.value with data.left70    rwa [equal, value]71  unfold polynomialVariablesUsed72  exact Finite.big_union with finite, members7374section Evaluation75variable (I A add z neg mul one v w : Set)76hypothesis ring : IsCommRing(A, add, z, neg, mul, one)77hypothesis first : v : I → A78hypothesis second : w : I → A7980theorem monomialEvaluate.agree_on_support (m : Set)81  requires monomial : m ∈ monomials(I)82  requires agreement : ∀ i ∈ functionSupport(m, I, 0), v(i) = w(i)83  shows monomialEvaluate(I, A, add, z, neg, mul, one, v)(m) = monomialEvaluate(I, A, add, z, neg, mul, one, w)(m)84proof85  have domain := functionSupport.subset at m, I, 086  have map := monomials.map with monomial87  have finite := CoefficientMap.finite_support with map88  have left := monomialWeights.function at I, functionSupport(m, I, 0), A, add, z, neg, mul, one, v, m with *89  have right := monomialWeights.function at I, functionSupport(m, I, 0), A, add, z, neg, mul, one, w, m with *90  have values : ∀ i ∈ functionSupport(m, I, 0), monomialWeights(I, functionSupport(m, I, 0), A, add, z, neg, mul, one, v, m)(i) = monomialWeights(I, functionSupport(m, I, 0), A, add, z, neg, mul, one, w, m)(i)91    intros i hi92    have valueV := monomialWeights.value at I, functionSupport(m, I, 0), A, add, z, neg, mul, one, v, m, i with *93    have valueW := monomialWeights.value at I, functionSupport(m, I, 0), A, add, z, neg, mul, one, w, m, i with *94    have equal := agreement with i, hi95    cc96  have equal := finiteRingProduct.congr with ring, finite, left, right, values97  have valueV := monomialEvaluate.value at I, A, add, z, neg, mul, one, v, m with *98  have valueW := monomialEvaluate.value at I, A, add, z, neg, mul, one, w, m with *99  cc100101theorem polynomialAt.agree_on_variables (p : Set)102  requires polynomial : p ∈ polynomials(I, A, z)103  requires agreement : ∀ i ∈ polynomialVariablesUsed(I, A, z, p), v(i) = w(i)104  shows polynomialAt(I, A, add, z, neg, mul, one, v)(p) = polynomialAt(I, A, add, z, neg, mul, one, w)(p)105proof106  have domain := functionSupport.subset at p, monomials(I), z107  have finite := polynomials.finite_support with polynomial108  have valuesV := monomialEvaluate.function at I, A, add, z, neg, mul, one, v with *109  have valuesW := monomialEvaluate.function at I, A, add, z, neg, mul, one, w with *110  have left := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), z), A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, v), p with *111  have right := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), z), A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, w), p with *112  have values : ∀ m ∈ functionSupport(p, monomials(I), z), polynomialEvaluationWeights(I, functionSupport(p, monomials(I), z), A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, v), p)(m) = polynomialEvaluationWeights(I, functionSupport(p, monomials(I), z), A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, w), p)(m)113    intros m hm114    have data := functionSupport.membership.forward with hm115    have same : ∀ i ∈ functionSupport(m, I, 0), v(i) = w(i)116      intros i hi117      have used : i ∈ polynomialVariablesUsed(I, A, z, p)118        exact polynomialVariablesUsed.membership.backward with ⟨m, hm, hi⟩119      exact agreement with i, used120    have equal := monomialEvaluate.agree_on_support with ring, first, second, data.left, same121    have valueV := polynomialEvaluationWeights.value at I, functionSupport(p, monomials(I), z), A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, v), p, m with *122    have valueW := polynomialEvaluationWeights.value at I, functionSupport(p, monomials(I), z), A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, w), p, m with *123    cc124  have equal := finiteRingSum.congr with ring, finite, left, right, values125  have valueV := polynomialEvaluate.value at I, A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, v), p with *126  have valueW := polynomialEvaluate.value at I, A, add, z, neg, mul, one, monomialEvaluate(I, A, add, z, neg, mul, one, w), p with *127  unfold polynomialAt128  cc129130end Evaluation131