Exponent-indexed coefficient maps on Hahn series

DefinitionExponent-indexed coefficient map on Hahn series#✓fully proved

Apply the map indexed by each exponent to the coefficient at that exponent.

noncomputable def gradedCoefficientMap (D : Γ → R →+ R) :
    HahnSeries Γ R →+ HahnSeries Γ R where
  toFun f :=
    { coeff := fun y => D y (f.coeff y)
      isPWO_support' := f.isPWO_support.mono fun y hy h => hy (by simp [h]) }
  map_zero' := by
    ext y
    simp
  map_add' f g := by
    ext y
    simp

Used by 6

Used byCoefficient formula for an exponent-indexed coefficient map · Exponent-indexed coefficient map on a constant series · Product rule for graded Leibniz coefficient maps · Exponent-indexed coefficient map on a single-term series · Exponent-indexed coefficient map of the zero family · Exponent-indexed coefficient maps do not enlarge the support

TheoremCoefficient formula for an exponent-indexed coefficient map#✓fully proved

The coefficient formula for an exponent-indexed coefficient map.

@[simp] theorem coeff_gradedCoefficientMap (D : Γ → R →+ R) (f : HahnSeries Γ R) (y : Γ) :
    (gradedCoefficientMap D f).coeff y = D y (f.coeff y)

Uses 1

Statement usesExponent-indexed coefficient map on Hahn series

TheoremExponent-indexed coefficient maps do not enlarge the support#✓fully proved

Acting coefficientwise cannot introduce new exponents into the support.

theorem support_gradedCoefficientMap (D : Γ → R →+ R) (f : HahnSeries Γ R) :
    (gradedCoefficientMap D f).support ⊆ f.support

Uses 1 · Used by 1

Statement usesExponent-indexed coefficient map on Hahn series

Used byProduct rule for graded Leibniz coefficient maps

TheoremExponent-indexed coefficient map of the zero family#✓fully proved

The family consisting of zero maps induces the zero additive map.

@[simp] theorem gradedCoefficientMap_zero_family :
    gradedCoefficientMap (Γ := Γ) (fun _ => (0 : R →+ R)) = 0

Uses 1

Statement usesExponent-indexed coefficient map on Hahn series

TheoremExponent-indexed coefficient map on a single-term series#✓fully proved

A one-term series keeps its exponent and applies the map indexed by that exponent.

@[simp] theorem gradedCoefficientMap_single (D : Γ → R →+ R) (y : Γ) (a : R) :
    gradedCoefficientMap D (single y a) = single y (D y a)

Uses 1 · Used by 1

Statement usesExponent-indexed coefficient map on Hahn series

Used byExponent-indexed coefficient map on a constant series

TheoremExponent-indexed coefficient map on a constant series#✓fully proved

On a constant series, the map indexed by zero acts on the constant coefficient.

@[simp] theorem gradedCoefficientMap_C (D : Γ → R →+ R) (a : R) :
    gradedCoefficientMap D (HahnSeries.C a) = HahnSeries.C (D 0 a)

Uses 2

Statement usesExponent-indexed coefficient map on Hahn series

Proof usesExponent-indexed coefficient map on a single-term series

TheoremProduct rule for graded Leibniz coefficient maps#✓fully proved

An exponent-indexed coefficient map satisfying the graded Leibniz identity obeys the product rule on Hahn series.

theorem gradedCoefficientMap_mul (D : Γ → R →+ R)
    (hD : ∀ i j a b, D (i + j) (a * b) = D i a * b + a * D j b)
    (f g : HahnSeries Γ R) :
    gradedCoefficientMap D (f * g) =
      gradedCoefficientMap D f * g + f * gradedCoefficientMap D g

Uses 2

Statement usesExponent-indexed coefficient map on Hahn series

Proof usesExponent-indexed coefficient maps do not enlarge the support

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.