Exponential of multivariate formal power series

DefinitionTruncated exponential of a multivariate power series#✓fully proved

The finite sum ∑ n < N, wⁿ/n!, defined without a constant coefficient restriction.

noncomputable def expTrunc (N : ℕ) (w : MvPowerSeries σ R) : MvPowerSeries σ R :=
  ∑ n ∈ range N, ((n.factorial : ℚ)⁻¹) • w ^ n

Used by 9

Used byCoefficients of the exponential via truncation · Coefficient of the exponential in a given degree · Coefficients of weighted rescaling of truncated exponentials · Formal exponential turns sums into products · Weighted rescaling commutes with truncated exponentials · Filtration-preserving endomorphisms commute with the formal exponential · Ring maps commute with truncated exponentials · Partial derivative of the formal exponential · Partial derivative of the truncated exponential

DefinitionExponential of a power series with zero constant coefficient#✓fully proved

The formal exponential of a series with zero constant coefficient, obtained by substituting it into Mathlib's canonical exponential power series.

noncomputable def expOfConstantCoeffZero (w : MvPowerSeries σ R)
    (hw : constantCoeff w = 0) : MvPowerSeries σ R :=
  substAlgHom (hasSubst_of_constantCoeff_zero (fun _ : Unit => hw)) (PowerSeries.exp R)

Used by 13

Used byCoefficients of the exponential via truncation · Coefficient of the exponential in a given degree · Weighted coefficient relation passes to formal exponentials · Constant coefficient of the formal exponential is one · Formal exponential turns sums into products · Multivariate exponential as substitution into exp · Weighted rescaling commutes with the formal exponential · Exponential of a variable · Exponential of the zero series is one · Filtration-preserving endomorphisms commute with the formal exponential · Coefficient ring maps commute with the formal exponential · Partial derivative of the formal exponential · The operator exponential commutes with the formal exponential

TheoremMultivariate exponential as substitution into exp#✓fully proved

The exponential API is the canonical univariate exponential substituted at w.

theorem expOfConstantCoeffZero_eq_subst (w : MvPowerSeries σ R)
    (hw : constantCoeff w = 0) :
    expOfConstantCoeffZero w hw = PowerSeries.subst w (PowerSeries.exp R)

Uses 1 · Used by 5

Statement usesExponential of a power series with zero constant coefficient

Used byCoefficients of the exponential via truncation · Constant coefficient of the formal exponential is one · Exponential of a variable · Exponential of the zero series is one · Coefficient ring maps commute with the formal exponential

TheoremCoefficients of the exponential via truncation#✓fully proved

A coefficient of the exponential is computed by any truncation extending past its degree. This is the exact finite-sum formula used by the source's degreewise constructor.

theorem coeff_expOfConstantCoeffZero (w : MvPowerSeries σ R) (hw : constantCoeff w = 0)
    (d : σ →₀ ℕ) {N : ℕ} (hN : d.degree < N) :
    coeff d (expOfConstantCoeffZero w hw) = coeff d (expTrunc N w)

Uses 3 · Used by 4

Statement usesExponential of a power series with zero constant coefficient · Truncated exponential of a multivariate power series

Proof usesMultivariate exponential as substitution into exp

Used byCoefficient of the exponential in a given degree · Formal exponential turns sums into products · Filtration-preserving endomorphisms commute with the formal exponential · Partial derivative of the formal exponential

TheoremCoefficient of the exponential in a given degree#✓fully proved

In particular, the coefficient of degree d.degree uses exactly the terms n ≤ d.degree.

theorem coeff_expOfConstantCoeffZero_degree (w : MvPowerSeries σ R)
    (hw : constantCoeff w = 0) (d : σ →₀ ℕ) :
    coeff d (expOfConstantCoeffZero w hw) = coeff d (expTrunc (d.degree + 1) w)

Uses 3 · Used by 2

Statement usesExponential of a power series with zero constant coefficient · Truncated exponential of a multivariate power series

Proof usesCoefficients of the exponential via truncation

Used byFormal exponential turns sums into products · Filtration-preserving endomorphisms commute with the formal exponential

TheoremConstant coefficient of the formal exponential is one#✓fully proved

The constant coefficient of the formal exponential is one.

@[simp] theorem constantCoeff_expOfConstantCoeffZero (w : MvPowerSeries σ R)
    (hw : constantCoeff w = 0) : constantCoeff (expOfConstantCoeffZero w hw) = 1

Uses 2

Statement usesExponential of a power series with zero constant coefficient

Proof usesMultivariate exponential as substitution into exp

TheoremExponential of the zero series is one#✓fully proved

The exponential of the zero series is one.

@[simp] theorem expOfConstantCoeffZero_zero :
    expOfConstantCoeffZero (0 : MvPowerSeries σ R) (map_zero _) = 1

Uses 2

Statement usesExponential of a power series with zero constant coefficient

Proof usesMultivariate exponential as substitution into exp

TheoremCoefficient ring maps commute with the formal exponential#✓fully proved

Applying a coefficient ring homomorphism commutes with the formal exponential.

theorem map_expOfConstantCoeffZero {S : Type*} [CommRing S] [Algebra ℚ S]
    (f : R →+* S) (w : MvPowerSeries σ R) (hw : constantCoeff w = 0) :
    map f (expOfConstantCoeffZero w hw) =
      expOfConstantCoeffZero (map f w) (by rw [constantCoeff_map, hw, map_zero])

Uses 2 · Used by 1

Statement usesExponential of a power series with zero constant coefficient

Proof usesMultivariate exponential as substitution into exp

Used byWeighted rescaling commutes with the formal exponential

TheoremExponential of a variable#✓fully proved

Substituting a variable recovers the canonical exponential in that variable.

@[simp] theorem expOfConstantCoeffZero_X (i : σ) :
    expOfConstantCoeffZero (X i : MvPowerSeries σ R) (constantCoeff_X i) =
      (PowerSeries.exp R).toMvPowerSeries i

Uses 2

Statement usesExponential of a power series with zero constant coefficient

Proof usesMultivariate exponential as substitution into exp

TheoremFormal exponential turns sums into products#✓fully proved

The formal exponential carries sums of series with zero constant coefficient to products.

theorem expOfConstantCoeffZero_add {a b : MvPowerSeries σ R}
    (ha : constantCoeff a = 0) (hb : constantCoeff b = 0) :
    expOfConstantCoeffZero (a + b) (by rw [map_add, ha, hb, add_zero]) =
      expOfConstantCoeffZero a ha * expOfConstantCoeffZero b hb

Uses 4

Statement usesExponential of a power series with zero constant coefficient

Proof usesCoefficients of the exponential via truncation · Coefficient of the exponential in a given degree · Truncated exponential of a multivariate power series

TheoremPartial derivative of the truncated exponential#✓fully proved

The partial derivative of the finite exponential sum containing the terms w ^ n / n! for n ≤ N is the derivative of its exponent times the sum containing those terms for n < N.

theorem pderiv_expTrunc (i : σ) (N : ℕ) (w : MvPowerSeries σ R) :
    pderiv i (expTrunc (N + 1) w) = pderiv i w * expTrunc N w

Uses 1 · Used by 1

Statement usesTruncated exponential of a multivariate power series

Used byPartial derivative of the formal exponential

TheoremPartial derivative of the formal exponential#✓fully proved

The partial derivative of the canonical exponential is the derivative of its exponent times the exponential.

theorem pderiv_expOfConstantCoeffZero (i : σ) {w : MvPowerSeries σ R}
    (hw : constantCoeff w = 0) :
    pderiv i (expOfConstantCoeffZero w hw) =
      pderiv i w * expOfConstantCoeffZero w hw

Uses 4

Statement usesExponential of a power series with zero constant coefficient

Proof usesCoefficients of the exponential via truncation · Truncated exponential of a multivariate power series · Partial derivative of the truncated exponential

TheoremRing maps commute with truncated exponentials#✓fully proved

A ring homomorphism between multivariate power-series rings commutes with finite exponential truncations.

theorem map_expTrunc {τ S : Type*} [CommRing S] [Algebra ℚ S]
    (Φ : MvPowerSeries σ R →+* MvPowerSeries τ S) (N : ℕ) (w : MvPowerSeries σ R) :
    Φ (expTrunc N w) = expTrunc N (Φ w)

Uses 1 · Used by 2

Statement usesTruncated exponential of a multivariate power series

Used byWeighted rescaling commutes with truncated exponentials · Filtration-preserving endomorphisms commute with the formal exponential

TheoremFiltration-preserving endomorphisms commute with the formal exponential#✓fully proved

A ring endomorphism preserving the total-degree coefficient filtration commutes with the formal exponential. The filtration premise itself implies that the image of a zero-constant series again has zero constant coefficient.

MvPowerSeries.hom_expOfConstantCoeffZero · 18 lines

theorem hom_expOfConstantCoeffZero
    (Φ : MvPowerSeries σ R →+* MvPowerSeries σ R)
    (hΦ : ∀ (d : σ →₀ ℕ) (f g : MvPowerSeries σ R),
      (∀ e : σ →₀ ℕ, e.degree ≤ d.degree → coeff e f = coeff e g) →
        coeff d (Φ f) = coeff d (Φ g))
    {w : MvPowerSeries σ R} (hw : constantCoeff w = 0) :
    Φ (expOfConstantCoeffZero w hw) =
      expOfConstantCoeffZero (Φ w) (by
        calc
          constantCoeff (Φ w) = coeff 0 (Φ w) :=
            (coeff_zero_eq_constantCoeff_apply _).symm
          _ = coeff 0 (Φ 0) := hΦ 0 w 0 (by
            intro e he
            have he0 : e = 0 := (Finsupp.degree_eq_zero_iff e).mp
              (Nat.eq_zero_of_le_zero (by simpa using he))
            subst e
            simp [coeff_zero_eq_constantCoeff_apply, hw])
          _ = 0 := by rw [map_zero, coeff_zero])

Uses 5 · Used by 2

Statement usesExponential of a power series with zero constant coefficient

Proof usesCoefficients of the exponential via truncation · Coefficient of the exponential in a given degree · Truncated exponential of a multivariate power series · Ring maps commute with truncated exponentials

Used byWeighted rescaling commutes with the formal exponential · The operator exponential commutes with the formal exponential

TheoremCoefficients of a weighted rescaling of a rational power series#✓fully proved

Mapping rational coefficients and rescaling variable i by ε ^ wt (Finsupp.single i 1) multiplies coefficient d by ε ^ wt d.

theorem coeff_rescale_map_of_weight {X R : Type*} [CommRing R] [Algebra ℚ R]
    (wt : (X →₀ ℕ) →+ ℕ) (ε : R) (q : MvPowerSeries X ℚ) (d : X →₀ ℕ) :
    coeff d
        (rescale (fun i => ε ^ wt (Finsupp.single i 1))
          (map (algebraMap ℚ R) q)) =
      algebraMap ℚ R (coeff d q) * ε ^ wt d

Used by 4

Used byWeighted coefficient relation passes to formal exponentials · Coefficients of weighted rescaling of truncated exponentials · Characterization of weighted rescalings of a power series · Weighted rescaling commutes with the formal exponential

TheoremCharacterization of weighted rescalings of a power series#✓fully proved

A series has the weighted coefficients of q exactly when it is the canonical coefficient map of q followed by the corresponding rescaling.

theorem eq_rescale_map_of_weight_iff {X R : Type*} [CommRing R] [Algebra ℚ R]
    (wt : (X →₀ ℕ) →+ ℕ) (ε : R) (q : MvPowerSeries X ℚ) (w : MvPowerSeries X R) :
    w = rescale (fun i => ε ^ wt (Finsupp.single i 1)) (map (algebraMap ℚ R) q) ↔
      ∀ d, coeff d w = algebraMap ℚ R (coeff d q) * ε ^ wt d

Uses 1 · Used by 1

Proof usesCoefficients of a weighted rescaling of a rational power series

Used byWeighted coefficient relation passes to formal exponentials

TheoremWeighted rescaling commutes with truncated exponentials#✓fully proved

Weighted coefficient mapping and rescaling commutes with every finite exponential truncation, without a constant coefficient restriction.

theorem expTrunc_rescale_map_of_weight (wt : (X →₀ ℕ) →+ ℕ) (ε : R)
    (q : MvPowerSeries X ℚ) (N : ℕ) :
    expTrunc N
        (rescale (fun i => ε ^ wt (Finsupp.single i 1))
          (map (algebraMap ℚ R) q)) =
      rescale (fun i => ε ^ wt (Finsupp.single i 1))
        (map (algebraMap ℚ R) (expTrunc N q))

Uses 2 · Used by 1

Statement usesTruncated exponential of a multivariate power series

Proof usesRing maps commute with truncated exponentials

Used byCoefficients of weighted rescaling of truncated exponentials

TheoremCoefficients of weighted rescaling of truncated exponentials#✓fully proved

The coefficient form of weighted finite exponential commutation. It preserves the source's degreewise expression for arbitrary input series.

theorem coeff_expTrunc_rescale_map_of_weight (wt : (X →₀ ℕ) →+ ℕ) (ε : R)
    (q : MvPowerSeries X ℚ) (N : ℕ) (d : X →₀ ℕ) :
    coeff d
        (expTrunc N
          (rescale (fun i => ε ^ wt (Finsupp.single i 1))
            (map (algebraMap ℚ R) q))) =
      algebraMap ℚ R (coeff d (expTrunc N q)) * ε ^ wt d

Uses 3

Statement usesTruncated exponential of a multivariate power series

Proof usesCoefficients of a weighted rescaling of a rational power series · Weighted rescaling commutes with truncated exponentials

TheoremWeighted rescaling commutes with the formal exponential#✓fully proved

On the zero-constant domain, weighted coefficient mapping and rescaling commutes with the lawful full formal exponential.

theorem expOfConstantCoeffZero_rescale_map_of_weight (wt : (X →₀ ℕ) →+ ℕ)
    (ε : R) (q : MvPowerSeries X ℚ) (hq : constantCoeff q = 0) :
    expOfConstantCoeffZero
        (rescale (fun i => ε ^ wt (Finsupp.single i 1))
          (map (algebraMap ℚ R) q)) (by
            rw [← coeff_zero_eq_constantCoeff_apply, coeff_rescale_map_of_weight,
              coeff_zero_eq_constantCoeff_apply, hq]
            simp) =
      rescale (fun i => ε ^ wt (Finsupp.single i 1))
        (map (algebraMap ℚ R) (expOfConstantCoeffZero q hq))

Uses 4 · Used by 1

Statement usesCoefficients of a weighted rescaling of a rational power series · Exponential of a power series with zero constant coefficient

Proof usesFiltration-preserving endomorphisms commute with the formal exponential · Coefficient ring maps commute with the formal exponential

Used byWeighted coefficient relation passes to formal exponentials

TheoremWeighted coefficient equality transfers zero constant coefficient#✓fully proved

Weighted coefficient equality transfers a zero constant coefficient from the rational source series to the target series.

theorem constantCoeff_eq_zero_of_weight (wt : (X →₀ ℕ) →+ ℕ) (ε : R)
    (q : MvPowerSeries X ℚ) {w : MvPowerSeries X R} (hq : constantCoeff q = 0)
    (hw : ∀ d, coeff d w = algebraMap ℚ R (coeff d q) * ε ^ wt d) :
    constantCoeff w = 0

Used by 1

Used byWeighted coefficient relation passes to formal exponentials

TheoremWeighted coefficient relation passes to formal exponentials#✓fully proved

If w has the coefficients of q scaled by an additive weight, then the same coefficient relation holds for their lawful formal exponentials. The coefficient hypothesis and q's zero constant imply the required premise for w; no separate zero-constant assumption on w is needed.

theorem coeff_expOfConstantCoeffZero_of_weight (wt : (X →₀ ℕ) →+ ℕ) (ε : R)
    (q : MvPowerSeries X ℚ) {w : MvPowerSeries X R} (hq : constantCoeff q = 0)
    (hw : ∀ d, coeff d w = algebraMap ℚ R (coeff d q) * ε ^ wt d)
    (d : X →₀ ℕ) :
    coeff d
        (expOfConstantCoeffZero w (constantCoeff_eq_zero_of_weight wt ε q hq hw)) =
      algebraMap ℚ R (coeff d (expOfConstantCoeffZero q hq)) * ε ^ wt d

Uses 5

Statement usesWeighted coefficient equality transfers zero constant coefficient · Exponential of a power series with zero constant coefficient

Proof usesCoefficients of a weighted rescaling of a rational power series · Characterization of weighted rescalings of a power series · Weighted rescaling commutes with the formal exponential

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.