Coefficientwise derivations of Hahn series

DefinitionCoefficientwise linear operator on Hahn series#✓fully proved

Apply a coefficient derivation to a Hahn series as an R-linear operator.

noncomputable def coefficientLinearMap (d : Derivation R A A) :
    HahnSeries Γ A →ₗ[R] HahnSeries Γ A where
  toFun f := f.map d
  map_add' f g := by
    ext y
    simp
  map_smul' q f := by
    ext y
    simp

Used by 3

Used byCoefficient formula for the coefficientwise linear operator · Coefficientwise derivation of Hahn series · Coefficientwise linear operator does not enlarge the support

TheoremCoefficient formula for the coefficientwise linear operator#✓fully proved

The coefficient formula for the linear operator underlying the lifted derivation.

@[simp] theorem coeff_coefficientLinearMap (d : Derivation R A A)
    (f : HahnSeries Γ A) (y : Γ) :
    (coefficientLinearMap d f).coeff y = d (f.coeff y)

Uses 1 · Used by 1

Statement usesCoefficientwise linear operator on Hahn series

Used byCoefficientwise derivation of Hahn series

TheoremCoefficientwise linear operator does not enlarge the support#✓fully proved

Acting on coefficients cannot introduce new exponents into the support.

theorem support_coefficientLinearMap (d : Derivation R A A)
    (f : HahnSeries Γ A) : (coefficientLinearMap d f).support ⊆ f.support

Uses 1 · Used by 1

Statement usesCoefficientwise linear operator on Hahn series

Used byCoefficientwise derivation of Hahn series

DefinitionCoefficientwise derivation of Hahn series#✓fully proved

Extend a derivation of the coefficient algebra by applying it to each coefficient.

noncomputable def coefficientDerivation (d : Derivation R A A) :
    Derivation R (HahnSeries Γ A) (HahnSeries Γ A) :=
  Derivation.mk' (coefficientLinearMap d) fun f g => by
    ext y
    rw [coeff_coefficientLinearMap, smul_eq_mul, smul_eq_mul, coeff_add, mul_comm g,
      coeff_mul, coeff_mul_right' g.isPWO_support (support_coefficientLinearMap d g),
      coeff_mul_left' f.isPWO_support (support_coefficientLinearMap d f), map_sum,
      ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun p _ => ?_
    rw [Derivation.leibniz, smul_eq_mul, smul_eq_mul, coeff_coefficientLinearMap,
      coeff_coefficientLinearMap, mul_comm (g.coeff p.2)]

Uses 3 · Used by 5

Statement usesCoefficient formula for the coefficientwise linear operator · Coefficientwise linear operator on Hahn series · Coefficientwise linear operator does not enlarge the support

Used byCoefficients of the coefficientwise derivation · Coefficientwise derivation of a constant series · Commuting derivations lift to commuting coefficientwise derivations · Coefficientwise derivation of a single-term series · Coefficientwise lift of the zero derivation

TheoremCoefficients of the coefficientwise derivation#✓fully proved

The coefficient of the lifted derivation is the derivative of that coefficient.

@[simp] theorem coeff_coefficientDerivation (d : Derivation R A A)
    (f : HahnSeries Γ A) (y : Γ) :
    (coefficientDerivation d f).coeff y = d (f.coeff y)

Uses 1 · Used by 1

Statement usesCoefficientwise derivation of Hahn series

Used byCoefficientwise derivation of a single-term series

TheoremCoefficientwise lift of the zero derivation#✓fully proved

The lift of the zero derivation is zero.

@[simp] theorem coefficientDerivation_zero :
    coefficientDerivation (Γ := Γ) (0 : Derivation R A A) = 0

Uses 1

Statement usesCoefficientwise derivation of Hahn series

TheoremCoefficientwise derivation of a single-term series#✓fully proved

A one-term series keeps its exponent and differentiates its coefficient.

@[simp] theorem coefficientDerivation_single (d : Derivation R A A) (y : Γ) (a : A) :
    coefficientDerivation d (single y a) = single y (d a)

Uses 2 · Used by 1

Statement usesCoefficientwise derivation of Hahn series

Proof usesCoefficients of the coefficientwise derivation

Used byCoefficientwise derivation of a constant series

TheoremCoefficientwise derivation of a constant series#✓fully proved

On a constant series, the lift acts on its constant coefficient.

@[simp] theorem coefficientDerivation_C (d : Derivation R A A) (a : A) :
    coefficientDerivation (Γ := Γ) d (HahnSeries.C a) = HahnSeries.C (d a)

Uses 2

Statement usesCoefficientwise derivation of Hahn series

Proof usesCoefficientwise derivation of a single-term series

TheoremCommuting derivations lift to commuting coefficientwise derivations#✓fully proved

Commuting coefficient derivations lift to commuting derivations of Hahn series.

theorem coefficientDerivation_commute {d d' : Derivation R A A}
    (h : Function.Commute d d') :
    Function.Commute (coefficientDerivation (Γ := Γ) d) (coefficientDerivation d')

Uses 1

Statement usesCoefficientwise derivation of Hahn series

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.