Positive weighted monomial substitutions

A weighted monomial substitution sends each source variable to one monomial with a specified natural coefficient. If every weight is positive, the weights affect coefficients but not support: the support is still the image of the source support under the linear exponent map.

This is the coefficient-aware extension of MonomialSubstitution needed for positive named constants. A positive scalar is represented by a monomial of exponent zero and that scalar as its weight.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.substitution {SourceVar : Type u} {TargetVar : Type v} (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (source : SourceVar) : MvPolynomial TargetVar ℕ

Send a source variable to a monomial with the prescribed exponent and coefficient.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.substitution weight basis source = (MvPolynomial.monomial (basis source)) (weight source)

def Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.coefficient {SourceVar : Type u} (weight : SourceVar → ℕ) (exponent : SourceVar →₀ ℕ) : ℕ

Product of the coefficient weights contributed by a source monomial.

Equations

• Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.coefficient weight exponent = exponent.prod fun (source : SourceVar) (power : ℕ) => weight source ^ power

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.monomialExpansion_eq {SourceVar : Type u} {TargetVar : Type v} (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (exponent : SourceVar →₀ ℕ) : Expansion.monomialExpansion (substitution weight basis) exponent = (MvPolynomial.monomial ((MonomialSubstitution.exponentMap basis) exponent)) (coefficient weight exponent)

A weighted monomial substitution still expands one monomial to one monomial; its exponent and coefficient are computed independently.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.coefficient_pos {SourceVar : Type u} (weight : SourceVar → ℕ) (positive : ∀ (source : SourceVar), 0 < weight source) (exponent : SourceVar →₀ ℕ) : 0 < coefficient weight exponent

Positivity of all variable weights implies positivity of every monomial coefficient produced by the substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.support_monomialExpansion_eq_if {SourceVar : Type u} {TargetVar : Type v} (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (exponent : SourceVar →₀ ℕ) : (Expansion.monomialExpansion (substitution weight basis) exponent).support = if coefficient weight exponent = 0 then ∅ else {(MonomialSubstitution.exponentMap basis) exponent}

Without a positivity assumption, a weighted monomial expansion is either zero or has the usual singleton exponent support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.support_monomialExpansion_subset {SourceVar : Type u} {TargetVar : Type v} (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (exponent : SourceVar →₀ ℕ) : (Expansion.monomialExpansion (substitution weight basis) exponent).support ⊆ {(MonomialSubstitution.exponentMap basis) exponent}

Even zero weights cannot create an exponent outside the ordinary linear image; they can only delete that image monomial.

@[simp]

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.support_monomialExpansion {SourceVar : Type u} {TargetVar : Type v} (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (positive : ∀ (source : SourceVar), 0 < weight source) (exponent : SourceVar →₀ ℕ) : (Expansion.monomialExpansion (substitution weight basis) exponent).support = {(MonomialSubstitution.exponentMap basis) exponent}

Under positive weights, every source monomial has singleton support at the ordinary linear exponent image.

noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.transform {SourceVar : Type u} {TargetVar : Type v} (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : MvPolynomial TargetVar ℕ

Apply a weighted monomial substitution to a polynomial.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.survivingSupport {SourceVar : Type u} (weight : SourceVar → ℕ) (polynomial : MvPolynomial SourceVar ℕ) : Finset (SourceVar →₀ ℕ)

Source monomials whose accumulated coefficient weight is nonzero.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.support_transform_eq_surviving_image {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : (transform weight basis polynomial).support = Finset.image (⇑(MonomialSubstitution.exponentMap basis)) (survivingSupport weight polynomial)

Exact support with arbitrary weights: discard source monomials killed by a zero accumulated weight, then apply the linear exponent map.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.support_transform {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (positive : ∀ (source : SourceVar), 0 < weight source) (polynomial : MvPolynomial SourceVar ℕ) : (transform weight basis polynomial).support = Finset.image (⇑(MonomialSubstitution.exponentMap basis)) polynomial.support

Exact support of a positive weighted monomial substitution.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.support_transform_subset_image {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : (transform weight basis polynomial).support ⊆ Finset.image (⇑(MonomialSubstitution.exponentMap basis)) polynomial.support

Arbitrary natural weights, including zero, can only delete monomials from the exponent image of the source support.

theorem Algebraic.Fusion.Arithmetic.Progress.Separated.WeightedMonomialSubstitution.card_support_transform_le {SourceVar : Type u} {TargetVar : Type v} [DecidableEq TargetVar] (weight : SourceVar → ℕ) (basis : SourceVar → TargetVar →₀ ℕ) (polynomial : MvPolynomial SourceVar ℕ) : (transform weight basis polynomial).support.card ≤ polynomial.support.card

A weighted monomial substitution never increases support cardinality, whether or not some weights vanish.