Exponentials of coefficient operators

DefinitionCoefficient operator on multivariate power series#✓fully proved

The operator ∑ i, X i * O i, defined by finite coefficient sums.

noncomputable def coefficientOperator (O : σ → A →ₗ[ℚ] A) :
    MvPowerSeries σ A →ₗ[ℚ] MvPowerSeries σ A := by
  classical
  exact LinearMap.pi fun d => ∑ i ∈ d.support,
    (O i).comp (LinearMap.proj (d - Finsupp.single i 1))

Used by 21

Used byIterated coefficient operators raise the order · Coefficient operators raise the order by one · Coefficient formula for a coefficient operator · Coefficient of a coefficient operator over any finite superset · Coefficients of the operator exponential via partial sums · Operator exponential coefficients depend only on lower-degree inputs · Low-degree coefficients of an iterated coefficient operator vanish · Product rule for coefficient operators · Lifted coefficient maps commute with the coefficient operator · Lifted coefficient maps commute with coefficient-operator iterates · The operator exponential preserves the constant coefficient · The exponential of coefficient derivations is multiplicative · Operator exponential when the square of the operator vanishes · The operator exponential fixes series annihilated by the operator · The exponential of coefficient derivations preserves one · Partial sums of the exponential of a coefficient operator · Partial operator exponential as a sum of function iterates · Exponential of the zero coefficient-operator family is the identity · Partial derivative of a coefficient operator · Partial derivative of partial sums of the operator exponential · Partial derivative of a coefficient-operator iterate

TheoremCoefficient formula for a coefficient operator#✓fully proved

The coefficient of the formal operator is a sum over the exponent support.

@[simp] theorem coeff_coefficientOperator (O : σ → A →ₗ[ℚ] A)
    (f : MvPowerSeries σ A) (d : σ →₀ ℕ) :
    coeff d (coefficientOperator O f) =
      ∑ i ∈ d.support, O i (coeff (d - Finsupp.single i 1) f)

Uses 1 · Used by 5

Statement usesCoefficient operator on multivariate power series

Used byCoefficient operators raise the order by one · Coefficient of a coefficient operator over any finite superset · Lifted coefficient maps commute with the coefficient operator · Operator exponential when the square of the operator vanishes · Exponential of the zero coefficient-operator family is the identity

TheoremCoefficient operators raise the order by one#✓fully proved

A coefficient operator raises every natural lower bound on order by one.

theorem add_one_le_order_coefficientOperator (O : σ → A →ₗ[ℚ] A)
    {f : MvPowerSeries σ A} {n : ℕ} (hf : (n : ℕ∞) ≤ f.order) :
    ((n + 1 : ℕ) : ℕ∞) ≤ (coefficientOperator O f).order

Uses 2 · Used by 1

Statement usesCoefficient operator on multivariate power series

Proof usesCoefficient formula for a coefficient operator

Used byIterated coefficient operators raise the order

TheoremIterated coefficient operators raise the order#✓fully proved

Iteration raises every natural lower bound on order by the number of steps.

theorem add_le_order_iterate_coefficientOperator (O : σ → A →ₗ[ℚ] A)
    {f : MvPowerSeries σ A} {d : ℕ} (hf : (d : ℕ∞) ≤ f.order) (n : ℕ) :
    ((d + n : ℕ) : ℕ∞) ≤ ((coefficientOperator O)^[n] f).order

Uses 2 · Used by 2

Statement usesCoefficient operator on multivariate power series

Proof usesCoefficient operators raise the order by one

Used byOperator exponential coefficients depend only on lower-degree inputs · Low-degree coefficients of an iterated coefficient operator vanish

TheoremLow-degree coefficients of an iterated coefficient operator vanish#✓fully proved

The nth iterate has no coefficient in total degree less than n.

theorem coeff_iterate_coefficientOperator_eq_zero (O : σ → A →ₗ[ℚ] A)
    (f : MvPowerSeries σ A) {d : σ →₀ ℕ} {n : ℕ} (hd : d.degree < n) :
    coeff d ((coefficientOperator O)^[n] f) = 0

Uses 2 · Used by 2

Statement usesCoefficient operator on multivariate power series

Proof usesIterated coefficient operators raise the order

Used byCoefficients of the operator exponential via partial sums · The exponential of coefficient derivations is multiplicative

TheoremCoefficient of a coefficient operator over any finite superset#✓fully proved

At any exponent, sum over any finite set containing its support.

theorem coeff_coefficientOperator_eq_sum (O : σ → A →ₗ[ℚ] A)
    (f : MvPowerSeries σ A) {d : σ →₀ ℕ} {s : Finset σ}
    (hs : d.support ⊆ s) :
    coeff d (coefficientOperator O f) =
      coeff d (∑ i ∈ s, (X i : MvPowerSeries σ A) *
        id (α := MvPowerSeries σ A) ((O i).compLeft (σ →₀ ℕ) f))

Uses 2 · Used by 2

Statement usesCoefficient operator on multivariate power series

Proof usesCoefficient formula for a coefficient operator

Used byProduct rule for coefficient operators · Partial derivative of a coefficient operator

TheoremPartial derivatives commute with coefficient lifting#✓fully proved

Partial differentiation commutes with canonical coefficient lifting.

theorem pderiv_compLeft (D : A →ₗ[ℚ] A) (i : σ) (f : MvPowerSeries σ A) :
    pderiv i (D.compLeft (σ →₀ ℕ) f) = D.compLeft (σ →₀ ℕ) (pderiv i f)

Used by 1

Used byPartial derivative of a coefficient operator

TheoremPartial derivative of a coefficient operator#✓fully proved

The operator derivative is the operator of the derivative plus the lifted O i.

theorem pderiv_coefficientOperator (O : σ → A →ₗ[ℚ] A) (i : σ)
    (f : MvPowerSeries σ A) :
    pderiv i (coefficientOperator O f) = coefficientOperator O (pderiv i f) +
      id (α := MvPowerSeries σ A) ((O i).compLeft (σ →₀ ℕ) f)

Uses 3 · Used by 1

Statement usesCoefficient operator on multivariate power series

Proof usesCoefficient of a coefficient operator over any finite superset · Partial derivatives commute with coefficient lifting

Used byPartial derivative of a coefficient-operator iterate

TheoremLifted coefficient maps commute with the coefficient operator#✓fully proved

Lifted coefficient maps commute with the operator under the source pairwise premise.

theorem compLeft_coefficientOperator {O : σ → A →ₗ[ℚ] A}
    (hc : ∀ i j a, O i (O j a) = O j (O i a)) (i : σ) (f : MvPowerSeries σ A) :
    (O i).compLeft (σ →₀ ℕ) (coefficientOperator O f) =
      coefficientOperator O ((O i).compLeft (σ →₀ ℕ) f)

Uses 2 · Used by 1

Statement usesCoefficient operator on multivariate power series

Proof usesCoefficient formula for a coefficient operator

Used byLifted coefficient maps commute with coefficient-operator iterates

TheoremProduct rule for coefficient operators#✓fully proved

A family of coefficient derivations gives the source product rule, without commutation.

theorem coefficientOperator_mul (D : σ → Derivation ℚ A A)
    (f g : MvPowerSeries σ A) :
    coefficientOperator (fun i => (D i).toLinearMap) (f * g) =
      f * coefficientOperator (fun i => (D i).toLinearMap) g +
      coefficientOperator (fun i => (D i).toLinearMap) f * g

Uses 2 · Used by 2

Statement usesCoefficient operator on multivariate power series

Proof usesCoefficient of a coefficient operator over any finite superset

Used byThe exponential of coefficient derivations is multiplicative · The exponential of coefficient derivations preserves one

DefinitionPartial sums of the exponential of a coefficient operator#✓fully proved

The first N operator iterates, ∑ n < N, 𝒪ⁿ / n!, acting on the full input series.

noncomputable def expOperatorPartial (O : σ → A →ₗ[ℚ] A) (N : ℕ) :
    MvPowerSeries σ A →ₗ[ℚ] MvPowerSeries σ A :=
  ∑ n ∈ Finset.range N, (n.factorial : ℚ)⁻¹ • coefficientOperator O ^ n

Uses 1 · Used by 10

Statement usesCoefficient operator on multivariate power series

Used byCoefficients of the operator exponential via partial sums · Operator exponential coefficients depend only on lower-degree inputs · Defining coefficient formula of the operator exponential · The operator exponential preserves the constant coefficient · Formal exponential of a coefficient operator · The exponential of coefficient derivations is multiplicative · Operator exponential when the square of the operator vanishes · Partial operator exponential as a sum of function iterates · Partial derivative of a coefficient-operator exponential · Partial derivative of partial sums of the operator exponential

TheoremPartial operator exponential as a sum of function iterates#✓fully proved

The finite exponential sum agrees with the source's function-iterate formula.

theorem expOperatorPartial_apply (O : σ → A →ₗ[ℚ] A) (N : ℕ)
    (f : MvPowerSeries σ A) :
    expOperatorPartial O N f =
      ∑ n ∈ Finset.range N, (n.factorial : ℚ)⁻¹ • (coefficientOperator O)^[n] f

Uses 2 · Used by 6

Statement usesCoefficient operator on multivariate power series · Partial sums of the exponential of a coefficient operator

Used byCoefficients of the operator exponential via partial sums · Operator exponential coefficients depend only on lower-degree inputs · The operator exponential preserves the constant coefficient · The exponential of coefficient derivations is multiplicative · Operator exponential when the square of the operator vanishes · Partial derivative of partial sums of the operator exponential

DefinitionFormal exponential of a coefficient operator#✓fully proved

The formal exponential: coefficient d uses operator iterates n ≤ d.degree.

noncomputable def expOperator (O : σ → A →ₗ[ℚ] A) :
    MvPowerSeries σ A →ₗ[ℚ] MvPowerSeries σ A :=
  LinearMap.pi fun d => (LinearMap.proj d).comp (expOperatorPartial O (d.degree + 1))

Uses 1 · Used by 14

Statement usesPartial sums of the exponential of a coefficient operator

Used byCoefficients of the operator exponential via partial sums · Operator exponential coefficients depend only on lower-degree inputs · Defining coefficient formula of the operator exponential · The operator exponential preserves the constant coefficient · The operator exponential commutes with the formal exponential · Exponential of coefficient derivations as a ring endomorphism · Evaluation of the operator-exponential ring homomorphism · The exponential of coefficient derivations is multiplicative · Operator exponential when the square of the operator vanishes · The operator exponential fixes series annihilated by the operator · The exponential of coefficient derivations preserves one · Exponential of the zero coefficient-operator family is the identity · Partial derivative of a coefficient-operator exponential · Gradient law for the exponential of commuting coefficient derivations

TheoremDefining coefficient formula of the operator exponential#✓fully proved

The defining iteration bound is exactly the source constructor's bound.

@[simp] theorem coeff_expOperator_def (O : σ → A →ₗ[ℚ] A)
    (f : MvPowerSeries σ A) (d : σ →₀ ℕ) :
    coeff d (expOperator O f) = coeff d (expOperatorPartial O (d.degree + 1) f)

Uses 2 · Used by 4

Statement usesFormal exponential of a coefficient operator · Partial sums of the exponential of a coefficient operator

Used byCoefficients of the operator exponential via partial sums · Operator exponential coefficients depend only on lower-degree inputs · The operator exponential preserves the constant coefficient · The exponential of coefficient derivations is multiplicative

TheoremCoefficients of the operator exponential via partial sums#✓fully proved

For d.degree < N, the first N operator iterates determine coefficient d.

theorem coeff_expOperator (O : σ → A →ₗ[ℚ] A) (f : MvPowerSeries σ A)
    {d : σ →₀ ℕ} {N : ℕ} (hd : d.degree < N) :
    coeff d (expOperator O f) = coeff d (expOperatorPartial O N f)

Uses 6 · Used by 3

Statement usesFormal exponential of a coefficient operator · Partial sums of the exponential of a coefficient operator

Proof usesDefining coefficient formula of the operator exponential · Low-degree coefficients of an iterated coefficient operator vanish · Coefficient operator on multivariate power series · Partial operator exponential as a sum of function iterates

Used byThe exponential of coefficient derivations is multiplicative · Operator exponential when the square of the operator vanishes · Partial derivative of a coefficient-operator exponential

TheoremThe operator exponential preserves the constant coefficient#✓fully proved

The formal exponential preserves every constant coefficient, including nonzero ones.

@[simp] theorem constantCoeff_expOperator (O : σ → A →ₗ[ℚ] A)
    (f : MvPowerSeries σ A) : constantCoeff (expOperator O f) = constantCoeff f

Uses 5 · Used by 1

Statement usesFormal exponential of a coefficient operator

Proof usesDefining coefficient formula of the operator exponential · Coefficient operator on multivariate power series · Partial sums of the exponential of a coefficient operator · Partial operator exponential as a sum of function iterates

Used byThe operator exponential commutes with the formal exponential

TheoremOperator exponential when the square of the operator vanishes#✓fully proved

If the second operator iterate vanishes on f, its exponential is f + 𝒪 f.

theorem expOperator_of_sq_zero (O : σ → A →ₗ[ℚ] A) {f : MvPowerSeries σ A}
    (hf : coefficientOperator O (coefficientOperator O f) = 0) :
    expOperator O f = f + coefficientOperator O f

Uses 6 · Used by 1

Statement usesCoefficient operator on multivariate power series · Formal exponential of a coefficient operator

Proof usesCoefficient formula for a coefficient operator · Coefficients of the operator exponential via partial sums · Partial sums of the exponential of a coefficient operator · Partial operator exponential as a sum of function iterates

Used byThe operator exponential fixes series annihilated by the operator

TheoremThe operator exponential fixes series annihilated by the operator#✓fully proved

The exponential fixes an input annihilated by the coefficient operator.

theorem expOperator_of_zero (O : σ → A →ₗ[ℚ] A) {f : MvPowerSeries σ A}
    (hf : coefficientOperator O f = 0) : expOperator O f = f

Uses 3 · Used by 2

Statement usesCoefficient operator on multivariate power series · Formal exponential of a coefficient operator

Proof usesOperator exponential when the square of the operator vanishes

Used byThe exponential of coefficient derivations preserves one · Exponential of the zero coefficient-operator family is the identity

TheoremExponential of the zero coefficient-operator family is the identity#✓fully proved

The exponential of the zero coefficient-map family is the identity linear map.

@[simp] theorem expOperator_zero_family :
    expOperator (fun _ : σ => (0 : A →ₗ[ℚ] A)) = LinearMap.id

Uses 4

Statement usesFormal exponential of a coefficient operator

Proof usesCoefficient formula for a coefficient operator · Coefficient operator on multivariate power series · The operator exponential fixes series annihilated by the operator

TheoremLifted coefficient maps commute with coefficient-operator iterates#✓fully proved

A lifted coefficient map commutes with every coefficient-operator iterate when the coefficient maps commute pairwise.

theorem compLeft_iterate_coefficientOperator {O : σ → A →ₗ[ℚ] A}
    (hc : ∀ i j a, O i (O j a) = O j (O i a)) (i : σ) (n : ℕ)
    (f : MvPowerSeries σ A) :
    (O i).compLeft (σ →₀ ℕ) ((coefficientOperator O)^[n] f) =
      (coefficientOperator O)^[n] ((O i).compLeft (σ →₀ ℕ) f)

Uses 2 · Used by 1

Statement usesCoefficient operator on multivariate power series

Proof usesLifted coefficient maps commute with the coefficient operator

Used byPartial derivative of a coefficient-operator iterate

TheoremPartial derivative of a coefficient-operator iterate#✓fully proved

The partial derivative of the (n + 1)st coefficient-operator iterate is the iterate of the partial derivative plus (n + 1) copies of the lifted coefficient map.

theorem pderiv_iterate_coefficientOperator {O : σ → A →ₗ[ℚ] A}
    (hc : ∀ i j a, O i (O j a) = O j (O i a)) (i : σ) (n : ℕ)
    (f : MvPowerSeries σ A) :
    pderiv i ((coefficientOperator O)^[n + 1] f) =
      (coefficientOperator O)^[n + 1] (pderiv i f) +
        (n + 1) • (coefficientOperator O)^[n] ((O i).compLeft (σ →₀ ℕ) f)

Uses 3 · Used by 1

Statement usesCoefficient operator on multivariate power series

Proof usesLifted coefficient maps commute with coefficient-operator iterates · Partial derivative of a coefficient operator

Used byPartial derivative of partial sums of the operator exponential

TheoremPartial derivative of partial sums of the operator exponential#✓fully proved

The partial derivative of the first N + 1 exponential terms is the corresponding partial sum on the derivative plus the first N terms on the lifted coefficient map.

theorem pderiv_expOperatorPartial {O : σ → A →ₗ[ℚ] A}
    (hc : ∀ i j a, O i (O j a) = O j (O i a)) (i : σ) (N : ℕ)
    (f : MvPowerSeries σ A) :
    pderiv i (expOperatorPartial O (N + 1) f) =
      expOperatorPartial O (N + 1) (pderiv i f) +
        expOperatorPartial O N ((O i).compLeft (σ →₀ ℕ) f)

Uses 4 · Used by 1

Statement usesPartial sums of the exponential of a coefficient operator

Proof usesCoefficient operator on multivariate power series · Partial operator exponential as a sum of function iterates · Partial derivative of a coefficient-operator iterate

Used byPartial derivative of a coefficient-operator exponential

TheoremPartial derivative of a coefficient-operator exponential#✓fully proved

The partial derivative of a formal coefficient-operator exponential is the exponential of the input derivative plus the exponential of the lifted coefficient map.

theorem pderiv_expOperator {O : σ → A →ₗ[ℚ] A}
    (hc : ∀ i j a, O i (O j a) = O j (O i a)) (i : σ)
    (f : MvPowerSeries σ A) :
    pderiv i (expOperator O f) =
      expOperator O (pderiv i f) +
        expOperator O ((O i).compLeft (σ →₀ ℕ) f)

Uses 4 · Used by 1

Statement usesFormal exponential of a coefficient operator

Proof usesCoefficients of the operator exponential via partial sums · Partial sums of the exponential of a coefficient operator · Partial derivative of partial sums of the operator exponential

Used byGradient law for the exponential of commuting coefficient derivations

TheoremGradient law for the exponential of commuting coefficient derivations#✓fully proved

The exponential gradient law specialized to a pairwise commuting family of coefficient derivations, using their canonical rational linear maps.

theorem pderiv_expOperator_derivation {D : σ → Derivation ℚ A A}
    (hc : ∀ i j a, D i (D j a) = D j (D i a)) (i : σ)
    (f : MvPowerSeries σ A) :
    pderiv i (expOperator (fun j => (D j).toLinearMap) f) =
      expOperator (fun j => (D j).toLinearMap) (pderiv i f) +
        expOperator (fun j => (D j).toLinearMap)
          ((D i).toLinearMap.compLeft (σ →₀ ℕ) f)

Uses 2

Statement usesFormal exponential of a coefficient operator

Proof usesPartial derivative of a coefficient-operator exponential

TheoremThe exponential of coefficient derivations is multiplicative#✓fully proved

The formal exponential of a family of coefficient derivations preserves products. No pairwise commutation or finiteness hypothesis on the family is needed.

theorem expOperator_mul (D : σ → Derivation ℚ A A) (f g : MvPowerSeries σ A) :
    expOperator (fun i => (D i).toLinearMap) (f * g) =
      expOperator (fun i => (D i).toLinearMap) f *
        expOperator (fun i => (D i).toLinearMap) g

Uses 9 · Used by 1

Statement usesFormal exponential of a coefficient operator

Proof usesFactorial-normalized iterated Leibniz rule · Coefficients of the operator exponential via partial sums · Defining coefficient formula of the operator exponential · Low-degree coefficients of an iterated coefficient operator vanish · Coefficient operator on multivariate power series · Product rule for coefficient operators · Partial sums of the exponential of a coefficient operator · Partial operator exponential as a sum of function iterates

Used byExponential of coefficient derivations as a ring endomorphism

TheoremThe exponential of coefficient derivations preserves one#✓fully proved

The formal exponential of a family of coefficient derivations preserves one.

@[simp] theorem expOperator_one (D : σ → Derivation ℚ A A) :
    expOperator (fun i => (D i).toLinearMap) (1 : MvPowerSeries σ A) = 1

Uses 4 · Used by 1

Statement usesFormal exponential of a coefficient operator

Proof usesCoefficient operator on multivariate power series · Product rule for coefficient operators · The operator exponential fixes series annihilated by the operator

Used byExponential of coefficient derivations as a ring endomorphism

DefinitionExponential of coefficient derivations as a ring endomorphism#✓fully proved

The formal exponential of coefficient derivations as a ring endomorphism.

noncomputable def expOperatorHom (D : σ → Derivation ℚ A A) :
    MvPowerSeries σ A →+* MvPowerSeries σ A where
  toFun := expOperator fun i => (D i).toLinearMap
  map_one' := expOperator_one D
  map_mul' := expOperator_mul D
  map_zero' := map_zero _
  map_add' := map_add _

Uses 3 · Used by 2

Statement usesFormal exponential of a coefficient operator · The exponential of coefficient derivations is multiplicative · The exponential of coefficient derivations preserves one

Used byThe operator exponential commutes with the formal exponential · Evaluation of the operator-exponential ring homomorphism

TheoremEvaluation of the operator-exponential ring homomorphism#✓fully proved

Applying the operator-exponential ring homomorphism is the existing formal operator exponential.

@[simp] theorem expOperatorHom_apply (D : σ → Derivation ℚ A A)
    (f : MvPowerSeries σ A) :
    expOperatorHom D f = expOperator (fun i => (D i).toLinearMap) f

Uses 2

Statement usesFormal exponential of a coefficient operator · Exponential of coefficient derivations as a ring endomorphism

TheoremOperator exponential coefficients depend only on lower-degree inputs#✓fully proved

A coefficient of the operator exponential depends only on input coefficients of no greater total degree.

theorem coeff_expOperator_congr (O : σ → A →ₗ[ℚ] A) (d : σ →₀ ℕ)
    (f g : MvPowerSeries σ A)
    (h : ∀ e : σ →₀ ℕ, e.degree ≤ d.degree → coeff e f = coeff e g) :
    coeff d (expOperator O f) = coeff d (expOperator O g)

Uses 6 · Used by 1

Statement usesFormal exponential of a coefficient operator

Proof usesIterated coefficient operators raise the order · Defining coefficient formula of the operator exponential · Coefficient operator on multivariate power series · Partial sums of the exponential of a coefficient operator · Partial operator exponential as a sum of function iterates

Used byThe operator exponential commutes with the formal exponential

TheoremThe operator exponential commutes with the formal exponential#✓fully proved

The operator exponential commutes with the lawful ordinary formal exponential.

theorem expOperator_expOfConstantCoeffZero (D : σ → Derivation ℚ A A)
    {w : MvPowerSeries σ A} (hw : constantCoeff w = 0) :
    expOperator (fun i => (D i).toLinearMap) (expOfConstantCoeffZero w hw) =
      expOfConstantCoeffZero (expOperator (fun i => (D i).toLinearMap) w)
        (by rw [constantCoeff_expOperator, hw])

Uses 6

Statement usesThe operator exponential preserves the constant coefficient · Exponential of a power series with zero constant coefficient · Formal exponential of a coefficient operator

Proof usesOperator exponential coefficients depend only on lower-degree inputs · Exponential of coefficient derivations as a ring endomorphism · Filtration-preserving endomorphisms commute with the formal exponential

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.