Exponentials and Logarithms of Formal Power Series

This file formalizes Section 7.8 (Exponentials and logarithms) from the Algebraic Combinatorics textbook. It develops the theory of exponential and logarithm operations on formal power series over ℚ-algebras.

Convention

Throughout this file, K is assumed to be a commutative ℚ-algebra (Convention 7.8.1 in the text). This allows division by positive integers.

Main Definitions

• PowerSeries.logbar: The FPS ∑_{n≥1} (-1)^{n-1}/n · x^n, the Mercator series for log(1+x).
• PowerSeries.expbar: The FPS exp - 1 = ∑_{n≥1} 1/n! · x^n.
• PowerSeries.PowerSeries₀: The set of FPS with constant term 0.
• PowerSeries.PowerSeries₁: The set of FPS with constant term 1.
• PowerSeries.Exp: The map g ↦ exp ∘ g from K⟦X⟧₀ to K⟦X⟧₁.
• PowerSeries.Log: The map f ↦ logbar ∘ (f - 1) from K⟦X⟧₁ to K⟦X⟧₀.
• PowerSeries.loder: The logarithmic derivative f'/f for FPS with constant term 1.

Main Results

• PowerSeries.derivative_exp: exp' = exp (Definition 7.8.2 / Proposition 7.8.3)
• PowerSeries.derivative_expbar: expbar' = exp (Proposition 7.8.3)
• PowerSeries.derivative_logbar: logbar' = (1+x)⁻¹ (Proposition 7.8.3)
• PowerSeries.derivative_exp_comp: (exp ∘ g)' = (exp ∘ g) · g' (Proposition 7.8.3(a))
• PowerSeries.derivative_expbar_comp: (expbar ∘ g)' = (exp ∘ g) · g' (Proposition 7.8.3(a))
• PowerSeries.derivative_logbar_comp: (logbar ∘ g)' = (1+g)⁻¹ · g' (Proposition 7.8.3(b))
• PowerSeries.expbar_comp_logbar: expbar ∘ logbar = x (Theorem 7.8.5)
• PowerSeries.logbar_comp_expbar: logbar ∘ expbar = x (Theorem 7.8.5)
• PowerSeries.Log_Exp and PowerSeries.Exp_Log: Exp and Log are mutually inverse (Lemma 7.8.8)
• PowerSeries.Exp_add: Exp(f + g) = Exp(f) · Exp(g) (Lemma 7.8.9)
• PowerSeries.Log_mul: Log(fg) = Log(f) + Log(g) (Lemma 7.8.9)
• PowerSeries.Exp_Log_groupIso: Exp is a group isomorphism (Theorem 7.8.11)
• PowerSeries.loder_mul: loder(fg) = loder(f) + loder(g) (Proposition 7.8.14)
• PowerSeries.loder_inv: loder(f⁻¹) = -loder(f) (Corollary 7.8.16)
• PowerSeries.Log_tprod: Log(∏ fᵢ) = ∑ Log(fᵢ) for infinite products (Proposition prop.fps.Exp-Log-infprod)
• PowerSeries.Exp_sum: Exp(∑ gᵢ) = ∏ Exp(gᵢ) for infinite sums (Proposition prop.fps.Exp-Log-infsum)

References

• [Darij Grinberg, Algebraic Combinatorics, Section 7.8]
• [Grinberg-Reiner, logexp, Lemma 0.4 and Theorem 0.1]

Tags

power series, exponential, logarithm, formal power series

Section 7.8.1: Definitions

noncomputable def PowerSeries.logbar (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries K

The logarithm series logbar = ∑_{n≥1} (-1)^{n-1}/n · x^n, which is the Mercator series for log(1+x). This is \overline{\log} in Definition 7.8.2 (def.fps.exp-log).

Equations

• PowerSeries.logbar K = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else (algebraMap ℚ K) ((-1) ^ (n - 1) / ↑n)

noncomputable def PowerSeries.expbar (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries K

The shifted exponential series expbar = exp - 1 = ∑_{n≥1} 1/n! · x^n. This is \overline{\exp} in Definition 7.8.2 (def.fps.exp-log).

Equations

• PowerSeries.expbar K = PowerSeries.exp K - 1

Basic coefficient lemmas

@[simp]

theorem PowerSeries.coeff_logbar {K : Type u_1} [CommRing K] [Algebra ℚ K] (n : ℕ) : (coeff n) (logbar K) = if n = 0 then 0 else (algebraMap ℚ K) ((-1) ^ (n - 1) / ↑n)

@[simp]

theorem PowerSeries.constantCoeff_logbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : constantCoeff (logbar K) = 0

@[simp]

theorem PowerSeries.coeff_expbar {K : Type u_1} [CommRing K] [Algebra ℚ K] (n : ℕ) : (coeff n) (expbar K) = if n = 0 then 0 else (algebraMap ℚ K) (1 / ↑n.factorial)

@[simp]

theorem PowerSeries.constantCoeff_expbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : constantCoeff (expbar K) = 0

theorem PowerSeries.expbar_eq_exp_sub_one {K : Type u_1} [CommRing K] [Algebra ℚ K] : expbar K = exp K - 1

Explicit coefficient values for Definition 7.8.2 (def.fps.exp-log)

These lemmas verify that our definitions match the textbook formulas:

• exp = ∑_{n≥0} (1/n!) x^n
• logbar = ∑_{n≥1} ((-1)^{n-1}/n) x^n
• expbar = ∑_{n≥1} (1/n!) x^n

@[simp]

theorem PowerSeries.coeff_exp_zero {K : Type u_1} [CommRing K] [Algebra ℚ K] : (coeff 0) (exp K) = 1

The first few coefficients of exp: [x⁰]exp = 1, [x¹]exp = 1.

@[simp]

theorem PowerSeries.coeff_exp_one {K : Type u_1} [CommRing K] [Algebra ℚ K] : (coeff 1) (exp K) = 1

@[simp]

theorem PowerSeries.coeff_logbar_zero {K : Type u_1} [CommRing K] [Algebra ℚ K] : (coeff 0) (logbar K) = 0

The first few coefficients of logbar: [x⁰]logbar = 0, [x¹]logbar = 1.

@[simp]

theorem PowerSeries.coeff_logbar_one {K : Type u_1} [CommRing K] [Algebra ℚ K] : (coeff 1) (logbar K) = 1

@[simp]

theorem PowerSeries.coeff_expbar_zero {K : Type u_1} [CommRing K] [Algebra ℚ K] : (coeff 0) (expbar K) = 0

The first few coefficients of expbar: [x⁰]expbar = 0, [x¹]expbar = 1.

@[simp]

theorem PowerSeries.coeff_expbar_one {K : Type u_1} [CommRing K] [Algebra ℚ K] : (coeff 1) (expbar K) = 1

theorem PowerSeries.logbar_eq_sum_alternating {K : Type u_1} [CommRing K] [Algebra ℚ K] : logbar K = mk fun (n : ℕ) => if n = 0 then 0 else (algebraMap ℚ K) ((-1) ^ (n - 1) / ↑n)

The logbar series can be expressed as x - x²/2 + x³/3 - x⁴/4 + ....

theorem PowerSeries.exp_constantCoeff {K : Type u_1} [CommRing K] [Algebra ℚ K] : constantCoeff (exp K) = 1

exp has constant term 1. This is part of Definition 7.8.2 (def.fps.exp-log).

theorem PowerSeries.logbar_constantCoeff {K : Type u_1} [CommRing K] [Algebra ℚ K] : constantCoeff (logbar K) = 0

logbar has constant term 0. This is part of Definition 7.8.2 (def.fps.exp-log).

theorem PowerSeries.expbar_constantCoeff {K : Type u_1} [CommRing K] [Algebra ℚ K] : constantCoeff (expbar K) = 0

expbar has constant term 0. This is part of Definition 7.8.2 (def.fps.exp-log).

theorem PowerSeries.exp_eq_one_add_expbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : exp K = 1 + expbar K

The relationship between exp and expbar: exp = 1 + expbar.

Section 7.8.2: The exponential and logarithm are inverse

noncomputable def PowerSeries.invOnePlusX (K : Type u_1) [CommRing K] [Algebra ℚ K] : PowerSeries K

The series (1+x)⁻¹ = ∑_{n≥0} (-1)^n x^n.

Equations

• PowerSeries.invOnePlusX K = PowerSeries.mk fun (n : ℕ) => (algebraMap ℚ K) ((-1) ^ n)

@[simp]

theorem PowerSeries.coeff_invOnePlusX {K : Type u_1} [CommRing K] [Algebra ℚ K] (n : ℕ) : (coeff n) (invOnePlusX K) = (algebraMap ℚ K) ((-1) ^ n)

theorem PowerSeries.derivative_logbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : (derivative K) (logbar K) = invOnePlusX K

The derivative of logbar is invOnePlusX. This is part of the proof of Proposition 7.8.3 (prop.fps.exp-log-der).

theorem PowerSeries.derivative_expbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : (derivative K) (expbar K) = exp K

The derivative of expbar equals exp. This is equation (7.8.3) in the proof of Proposition 7.8.3 (prop.fps.exp-log-der).

theorem PowerSeries.derivative_exp_comp {K : Type u_1} [CommRing K] [Algebra ℚ K] {g : PowerSeries K} (hg : constantCoeff g = 0) : (derivative K) (subst g (exp K)) = subst g (exp K) * (derivative K) g

Chain rule for composition with exp: (exp ∘ g)' = (exp ∘ g) · g'. This is Proposition 7.8.3(a) (prop.fps.exp-log-der).

theorem PowerSeries.derivative_expbar_comp {K : Type u_1} [CommRing K] [Algebra ℚ K] {g : PowerSeries K} (hg : constantCoeff g = 0) : (derivative K) (subst g (expbar K)) = subst g (exp K) * (derivative K) g

Chain rule for composition with expbar: (expbar ∘ g)' = (exp ∘ g) · g'. This is Proposition 7.8.3(a) (prop.fps.exp-log-der).

Note that expbar = exp - 1, so expbar' = exp' = exp, and the chain rule gives (expbar ∘ g)' = (exp ∘ g) · g'.

theorem PowerSeries.invOnePlusX_mul_one_add_X {K : Type u_2} [Field K] [Algebra ℚ K] : invOnePlusX K * (1 + X) = 1

invOnePlusX K * (1 + X) = 1.

theorem PowerSeries.invOnePlusX_subst_eq_inv {K : Type u_2} [Field K] [Algebra ℚ K] {g : PowerSeries K} (hg : constantCoeff g = 0) : subst g (invOnePlusX K) = (1 + g)⁻¹

(invOnePlusX K).subst g = (1 + g)⁻¹ when constantCoeff g = 0.

theorem PowerSeries.derivative_logbar_comp {K : Type u_2} [Field K] [Algebra ℚ K] {g : PowerSeries K} (hg : constantCoeff g = 0) : (derivative K) (subst g (logbar K)) = (1 + g)⁻¹ * (derivative K) g

Chain rule for composition with logbar: (logbar ∘ g)' = (1+g)⁻¹ · g'. This is Proposition 7.8.3(b) (prop.fps.exp-log-der). Note: Requires Field K for the inverse to exist.

theorem PowerSeries.logbar_comp_expbar' {K : Type u_2} [Field K] [Algebra ℚ K] : subst (expbar K) (logbar K) = X

logbar ∘ expbar = x for fields. This is the second part of Theorem 7.8.5 (thm.fps.exp-log-inv), equation (7.8.1).

The proof strategy (from the textbook) is to show that logbar ∘ expbar and X have:

1. The same constant term (both are 0)
2. The same derivative (both equal 1) Then by Theorem 7.3.7(h), they must be equal.

For the derivative calculation:

• (logbar ∘ expbar)' = (logbar' ∘ expbar) · expbar' by chain rule
• logbar' = (1+X)⁻¹ and expbar' = exp
• (1+X)⁻¹ ∘ expbar = (1 + expbar)⁻¹ = exp⁻¹ since 1 + expbar = exp
• So (logbar ∘ expbar)' = exp⁻¹ · exp = 1 = X'

Note: This version is for fields. The general CommRing version is logbar_comp_expbar.

theorem PowerSeries.constantCoeff_subst_of_constantCoeff_zero {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hg : constantCoeff g = 0) : constantCoeff (subst g f) = constantCoeff f

The constant term of a composition f ∘ g where g has constant term 0. This is Lemma 7.8.4 (lem.fps.compos-cst-term-0).

Note: Mathlib has PowerSeries.constantCoeff_subst which requires HasSubst.

theorem PowerSeries.eq_of_derivative_eq_mul_of_inv {K : Type u_1} [CommRing K] [Algebra ℚ K] {h₁ h₂ g : PowerSeries K} (hd₁ : (derivative K) h₁ = (1 + h₁) * g) (hd₂ : (derivative K) h₂ = (1 + h₂) * g) (hc : constantCoeff h₁ = constantCoeff h₂) : h₁ = h₂

Uniqueness lemma for ODEs of the form h' = (1 + h) * g with matching initial conditions. This is used to prove expbar_comp_logbar.

theorem PowerSeries.expbar_comp_logbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : subst (logbar K) (expbar K) = X

expbar ∘ logbar = x. This is the first part of Theorem 7.8.5 (thm.fps.exp-log-inv), equation (7.8.1).

The proof uses the uniqueness of solutions to ODEs: both expbar ∘ logbar and X satisfy the ODE h' = (1 + h) * invOnePlusX with initial condition h(0) = 0.

theorem PowerSeries.invOnePlusX_subst_expbar_mul_exp {K : Type u_1} [CommRing K] [Algebra ℚ K] : subst (expbar K) (invOnePlusX K) * exp K = 1

(invOnePlusX K).subst (expbar K) * exp K = 1. This is a key lemma for proving logbar_comp_expbar.

theorem PowerSeries.eq_of_derivative_eq_one {K : Type u_1} [CommRing K] [Algebra ℚ K] {h₁ h₂ : PowerSeries K} (hd₁ : (derivative K) h₁ = 1) (hd₂ : (derivative K) h₂ = 1) (hc : constantCoeff h₁ = constantCoeff h₂) : h₁ = h₂

Uniqueness lemma for ODEs of the form h' = 1 (constant) with matching initial conditions.

theorem PowerSeries.logbar_comp_expbar {K : Type u_1} [CommRing K] [Algebra ℚ K] : subst (expbar K) (logbar K) = X

logbar ∘ expbar = x. This is the second part of Theorem 7.8.5 (thm.fps.exp-log-inv), equation (7.8.1).

The proof uses the uniqueness of solutions to ODEs: both logbar ∘ expbar and X satisfy the ODE h' = 1 with initial condition h(0) = 0. The key calculation is:

• (logbar ∘ expbar)' = (logbar' ∘ expbar) · expbar' by chain rule
• logbar' = invOnePlusX and expbar' = exp
• (invOnePlusX ∘ expbar) · exp = 1 since invOnePlusX · (1 + X) = 1 and 1 + expbar = exp
• So (logbar ∘ expbar)' = 1 = X'

Section 7.8.3: The exponential and logarithm of an FPS

def PowerSeries.PowerSeries₀ {R : Type u_2} [CommRing R] : Set (PowerSeries R)

R⟦X⟧₀ is the set of FPS with constant term 0. This is Definition 7.8.6(a) (def.fps.Exp-Log-maps).

Equations

• PowerSeries.PowerSeries₀ = {f : PowerSeries R | PowerSeries.constantCoeff f = 0}

def PowerSeries.PowerSeries₁ {R : Type u_2} [CommRing R] : Set (PowerSeries R)

R⟦X⟧₁ is the set of FPS with constant term 1. This is Definition 7.8.6(b) (def.fps.Exp-Log-maps).

Equations

• PowerSeries.PowerSeries₁ = {f : PowerSeries R | PowerSeries.constantCoeff f = 1}

theorem PowerSeries.mem_PowerSeries₀_iff {R : Type u_2} [CommRing R] {f : PowerSeries R} : f ∈ PowerSeries₀ ↔ constantCoeff f = 0

theorem PowerSeries.mem_PowerSeries₁_iff {R : Type u_2} [CommRing R] {f : PowerSeries R} : f ∈ PowerSeries₁ ↔ constantCoeff f = 1

theorem PowerSeries.X_mem_PowerSeries₀ {R : Type u_2} [CommRing R] : X ∈ PowerSeries₀

theorem PowerSeries.PowerSeries₀.zero_mem {R : Type u_2} [CommRing R] : 0 ∈ PowerSeries₀

R⟦X⟧₀ is closed under addition and subtraction and contains 0. This is Proposition 7.8.10(a) (prop.fps.Exp-Log-groups).

theorem PowerSeries.PowerSeries₀.add_mem {R : Type u_2} [CommRing R] {f g : PowerSeries R} (hf : f ∈ PowerSeries₀) (hg : g ∈ PowerSeries₀) : f + g ∈ PowerSeries₀

theorem PowerSeries.PowerSeries₀.neg_mem {R : Type u_2} [CommRing R] {f : PowerSeries R} (hf : f ∈ PowerSeries₀) : -f ∈ PowerSeries₀

theorem PowerSeries.PowerSeries₀.sub_mem {R : Type u_2} [CommRing R] {f g : PowerSeries R} (hf : f ∈ PowerSeries₀) (hg : g ∈ PowerSeries₀) : f - g ∈ PowerSeries₀

theorem PowerSeries.PowerSeries₁.one_mem {R : Type u_2} [CommRing R] : 1 ∈ PowerSeries₁

R⟦X⟧₁ is closed under multiplication and division and contains 1. This is Proposition 7.8.10(b) (prop.fps.Exp-Log-groups).

theorem PowerSeries.PowerSeries₁.mul_mem {R : Type u_2} [CommRing R] {f g : PowerSeries R} (hf : f ∈ PowerSeries₁) (hg : g ∈ PowerSeries₁) : f * g ∈ PowerSeries₁

theorem PowerSeries.sub_one_mem_PowerSeries₀ {R : Type u_2} [CommRing R] {f : PowerSeries R} (hf : f ∈ PowerSeries₁) : f - 1 ∈ PowerSeries₀

If f has constant term 1, then f - 1 has constant term 0. This is Lemma 7.8.7(d) (lem.fps.Exp-Log-maps-wd).

def PowerSeries.PowerSeries₀.addSubgroup {R : Type u_2} [CommRing R] : AddSubgroup (PowerSeries R)

R⟦X⟧₀ forms an additive subgroup. This is Proposition 7.8.10(a) (prop.fps.Exp-Log-groups).

Equations

• PowerSeries.PowerSeries₀.addSubgroup = { carrier := PowerSeries.PowerSeries₀, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem PowerSeries.PowerSeries₁.inv_mem {R : Type u_2} [Field R] {f : PowerSeries R} (hf : f ∈ PowerSeries₁) : f⁻¹ ∈ PowerSeries₁

theorem PowerSeries.PowerSeries₁.div_mem {R : Type u_2} [Field R] {f g : PowerSeries R} (hf : f ∈ PowerSeries₁) (hg : g ∈ PowerSeries₁) : f * g⁻¹ ∈ PowerSeries₁

Division in R⟦X⟧₁: if f, g ∈ R⟦X⟧₁, then f * g⁻¹ ∈ R⟦X⟧₁. This is part of Proposition 7.8.10(b) (prop.fps.Exp-Log-groups).

def PowerSeries.PowerSeries₁.subgroup {R : Type u_2} [Field R] : Subgroup (PowerSeries R)ˣ

R⟦X⟧₁ forms a multiplicative subgroup of units. This is Proposition 7.8.10(b) (prop.fps.Exp-Log-groups).

Equations

• PowerSeries.PowerSeries₁.subgroup = { carrier := {u : (PowerSeries R)ˣ | ↑u ∈ PowerSeries.PowerSeries₁}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem PowerSeries.exp_mem_PowerSeries₁ (K : Type u_2) [CommRing K] [Algebra ℚ K] : exp K ∈ PowerSeries₁

theorem PowerSeries.logbar_mem_PowerSeries₀ (K : Type u_2) [CommRing K] [Algebra ℚ K] : logbar K ∈ PowerSeries₀

theorem PowerSeries.expbar_mem_PowerSeries₀ (K : Type u_2) [CommRing K] [Algebra ℚ K] : expbar K ∈ PowerSeries₀

theorem PowerSeries.PowerSeries₀.subst_mem {K : Type u_2} [CommRing K] {f g : PowerSeries K} (hf : f ∈ PowerSeries₀) (hg : g ∈ PowerSeries₀) : subst g f ∈ PowerSeries₀

Composition of two FPS with constant term 0 has constant term 0. This is Lemma 7.8.7(a) (lem.fps.Exp-Log-maps-wd).

theorem PowerSeries.PowerSeries₁.subst_mem {K : Type u_2} [CommRing K] {f g : PowerSeries K} (hf : f ∈ PowerSeries₁) (hg : g ∈ PowerSeries₀) : subst g f ∈ PowerSeries₁

Composition of an FPS with constant term 1 and one with constant term 0 has constant term 1. This is Lemma 7.8.7(b) (lem.fps.Exp-Log-maps-wd).

theorem PowerSeries.exp_subst_mem_PowerSeries₁ {K : Type u_2} [CommRing K] [Algebra ℚ K] {g : PowerSeries K} (hg : g ∈ PowerSeries₀) : subst g (exp K) ∈ PowerSeries₁

exp ∘ g has constant term 1 when g has constant term 0. This is Lemma 7.8.7(c) (lem.fps.Exp-Log-maps-wd).

theorem PowerSeries.logbar_subst_sub_one_mem_PowerSeries₀ {K : Type u_2} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : f ∈ PowerSeries₁) : subst (f - 1) (logbar K) ∈ PowerSeries₀

noncomputable def PowerSeries.Exp {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries₀) : ↑PowerSeries₁

The exponential map Exp : K⟦X⟧₀ → K⟦X⟧₁ defined by g ↦ exp ∘ g. This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).

Equations

• PowerSeries.Exp g = ⟨PowerSeries.subst (↑g) (PowerSeries.exp K), ⋯⟩

noncomputable def PowerSeries.Log {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries₁) : ↑PowerSeries₀

The logarithm map Log : K⟦X⟧₁ → K⟦X⟧₀ defined by f ↦ logbar ∘ (f - 1). This is Definition 7.8.6(c) (def.fps.Exp-Log-maps).

Equations

• PowerSeries.Log f = ⟨PowerSeries.subst (↑f - 1) (PowerSeries.logbar K), ⋯⟩

theorem PowerSeries.Exp_val {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries₀) : ↑(Exp g) = subst (↑g) (exp K)

theorem PowerSeries.Log_val {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries₁) : ↑(Log f) = subst (↑f - 1) (logbar K)

theorem PowerSeries.Log_Exp {K : Type u_2} [CommRing K] [Algebra ℚ K] (g : ↑PowerSeries₀) : Log (Exp g) = g

Log (Exp g) = g for any g ∈ K⟦X⟧₀. This is part of Lemma 7.8.8 (lem.fps.Exp-Log-maps-inv).

theorem PowerSeries.Exp_Log {K : Type u_2} [CommRing K] [Algebra ℚ K] (f : ↑PowerSeries₁) : Exp (Log f) = f

theorem PowerSeries.Exp_Log_inverse {K : Type u_2} [CommRing K] [Algebra ℚ K] : Function.LeftInverse Log Exp ∧ Function.RightInverse Log Exp

Exp and Log are mutually inverse. This is Lemma 7.8.8 (lem.fps.Exp-Log-maps-inv).

Section 7.8.4: Addition to multiplication

theorem PowerSeries.eq_of_derivative_eq_mul_self {K : Type u_2} [CommRing K] [Algebra ℚ K] {h₁ h₂ g : PowerSeries K} (hd₁ : (derivative K) h₁ = h₁ * g) (hd₂ : (derivative K) h₂ = h₂ * g) (hc : constantCoeff h₁ = constantCoeff h₂) : h₁ = h₂

Uniqueness lemma: if two power series satisfy the same first-order linear ODE h' = h * g with the same initial condition, they are equal. This is used to prove Exp_add.

theorem PowerSeries.Exp_add {K : Type u_2} [CommRing K] [Algebra ℚ K] (f g : ↑PowerSeries₀) : Exp ⟨↑f + ↑g, ⋯⟩ = ⟨↑(Exp f) * ↑(Exp g), ⋯⟩

Exp(f + g) = Exp(f) · Exp(g). This is Lemma 7.8.9(a) (lem.fps.Exp-Log-additive).

theorem PowerSeries.Log_mul {K : Type u_2} [CommRing K] [Algebra ℚ K] (f g : ↑PowerSeries₁) : Log ⟨↑f * ↑g, ⋯⟩ = ⟨↑(Log f) + ↑(Log g), ⋯⟩

Log(fg) = Log(f) + Log(g). This is Lemma 7.8.9(b) (lem.fps.Exp-Log-additive).

theorem PowerSeries.Exp_isAddGroupHom {K : Type u_2} [CommRing K] [Algebra ℚ K] (f g : ↑PowerSeries₀) : Exp ⟨↑f + ↑g, ⋯⟩ = ⟨↑(Exp f) * ↑(Exp g), ⋯⟩

Exp : (K⟦X⟧₀, +, 0) → (K⟦X⟧₁, ·, 1) is a group homomorphism. This is part of Theorem 7.8.11 (thm.fps.Exp-Log-group-iso).

theorem PowerSeries.Exp_zero {K : Type u_2} [CommRing K] [Algebra ℚ K] : Exp ⟨0, ⋯⟩ = ⟨1, ⋯⟩

Exp(0) = 1.

theorem PowerSeries.Log_one {K : Type u_2} [CommRing K] [Algebra ℚ K] : Log ⟨1, ⋯⟩ = ⟨0, ⋯⟩

Log(1) = 0.

theorem PowerSeries.Exp_Log_groupIso {K : Type u_2} [CommRing K] [Algebra ℚ K] : (Function.LeftInverse Log Exp ∧ Function.RightInverse Log Exp) ∧ (∀ (f g : ↑PowerSeries₀), Exp ⟨↑f + ↑g, ⋯⟩ = ⟨↑(Exp f) * ↑(Exp g), ⋯⟩) ∧ Exp ⟨0, ⋯⟩ = ⟨1, ⋯⟩

Theorem 7.8.11 (thm.fps.Exp-Log-group-iso): The maps Exp and Log are mutually inverse group isomorphisms between (K⟦X⟧₀, +, 0) and (K⟦X⟧₁, ·, 1).

This means:

1. Exp is a bijection with inverse Log
2. Exp(f + g) = Exp(f) · Exp(g) for all f, g ∈ K⟦X⟧₀
3. Exp(0) = 1

Equivalently:

1. Log is a bijection with inverse Exp
2. Log(f · g) = Log(f) + Log(g) for all f, g ∈ K⟦X⟧₁
3. Log(1) = 0

The proof combines:

• Log_Exp and Exp_Log: mutual inverse property (Lemma 7.8.8)
• Exp_add: Exp preserves addition→multiplication (Lemma 7.8.9(a))
• Log_mul: Log preserves multiplication→addition (Lemma 7.8.9(b))

Section 7.8.5: The logarithmic derivative

noncomputable def PowerSeries.loder {R : Type u_2} [Field R] (f : PowerSeries R) : PowerSeries R

Definition 7.8.12 (def.fps.loder.1): The logarithmic derivative.

For any FPS f ∈ R⟦X⟧₁ (i.e., with constant term 1), we define the logarithmic derivative loder f ∈ R⟦X⟧ to be the FPS f'/f.

This is well-defined since f is invertible when constantCoeff f = 1 (see isUnit_of_constantCoeff_eq_one).

Important: This definition does NOT require R to be a ℚ-algebra. The definition makes sense over any field. The name "logarithmic derivative" comes from Proposition 7.8.13 (loder_eq_derivative_Log), which shows that over ℚ-algebras, loder f = (Log f)'.

Properties

• loder_one: loder 1 = 0
• loder_mul: loder(fg) = loder f + loder g (Proposition 7.8.14)
• loder_inv: loder(f⁻¹) = -loder f (Corollary 7.8.16)
• loder_prod: loder(∏ fᵢ) = ∑ loder fᵢ (Corollary 7.8.15)

Equations

• f.loder = (PowerSeries.derivative R) f * f⁻¹

theorem PowerSeries.loder_def {R : Type u_2} [Field R] (f : PowerSeries R) : f.loder = (derivative R) f * f⁻¹

The definition of the logarithmic derivative: loder f = f' * f⁻¹.

Well-definedness of loder (def.fps.loder.1)

The logarithmic derivative is well-defined for FPS with constant term 1 because such FPS are invertible. The following lemmas establish this.

theorem PowerSeries.isUnit_of_constantCoeff_eq_one {R : Type u_2} [Field R] {f : PowerSeries R} (hf : constantCoeff f = 1) : IsUnit f

An FPS with constant term 1 is invertible (a unit). This is the well-definedness statement for loder in Definition 7.8.12 (def.fps.loder.1).

The proof: If constantCoeff f = 1, then constantCoeff f is a unit in R, so by Proposition prop.fps.invertible, f is invertible in R⟦X⟧.

theorem PowerSeries.isUnit_iff_constantCoeff_isUnit {R : Type u_2} [Field R] {f : PowerSeries R} : IsUnit f ↔ IsUnit (constantCoeff f)

An FPS is invertible iff its constant coefficient is a unit. This is a more general version of isUnit_of_constantCoeff_eq_one.

theorem PowerSeries.mul_inv_cancel_of_constantCoeff_eq_one {R : Type u_2} [Field R] {f : PowerSeries R} (hf : constantCoeff f = 1) : f * f⁻¹ = 1

For FPS with constant term 1, we have f * f⁻¹ = 1. This is a key property used in the definition of loder.

theorem PowerSeries.inv_mul_cancel_of_constantCoeff_eq_one {R : Type u_2} [Field R] {f : PowerSeries R} (hf : constantCoeff f = 1) : f⁻¹ * f = 1

For FPS with constant term 1, we have f⁻¹ * f = 1.

theorem PowerSeries.constantCoeff_inv_of_constantCoeff_eq_one {R : Type u_2} [Field R] {f : PowerSeries R} (hf : constantCoeff f = 1) : constantCoeff f⁻¹ = 1

The inverse of an FPS with constant term 1 also has constant term 1.

theorem PowerSeries.invOnePlusX_eq_inv {R : Type u_2} [Field R] [Algebra ℚ R] : invOnePlusX R = (1 + X)⁻¹

The series invOnePlusX equals (1 + X)⁻¹.

theorem PowerSeries.subst_inv_of_mul_eq_one {R : Type u_2} [Field R] {g a b : PowerSeries R} (hg : HasSubst g) (hab : a * b = 1) : (subst g a)⁻¹ = subst g b

Helper lemma: if a * b = 1, then (a.subst g)⁻¹ = b.subst g.

theorem PowerSeries.loder_eq_derivative_Log {R : Type u_2} [Field R] [Algebra ℚ R] {f : PowerSeries R} (hf : constantCoeff f = 1) : f.loder = (derivative R) (subst (f - 1) (logbar R))

The logarithmic derivative equals the derivative of the logarithm over ℚ-algebras. This is Proposition 7.8.13 (prop.fps.loder.log).

theorem PowerSeries.loder_mul {R : Type u_2} [Field R] {f g : PowerSeries R} (hf : constantCoeff f = 1) (hg : constantCoeff g = 1) : (f * g).loder = f.loder + g.loder

The logarithmic derivative is additive under multiplication: loder(fg) = loder(f) + loder(g). This is Proposition 7.8.14 (prop.fps.loder.prod).

Note: This does NOT require R to be a ℚ-algebra.

theorem PowerSeries.loder_prod {R : Type u_2} [Field R] {ι : Type u_3} (s : Finset ι) (f : ι → PowerSeries R) (hf : ∀ i ∈ s, constantCoeff (f i) = 1) : (∏ i ∈ s, f i).loder = ∑ i ∈ s, (f i).loder

The logarithmic derivative of a product of k FPSs. This is Corollary 7.8.15 (cor.fps.loder.prodk).

Note: This does NOT require R to be a ℚ-algebra.

theorem PowerSeries.loder_inv {R : Type u_2} [Field R] {f : PowerSeries R} (hf : constantCoeff f = 1) : f⁻¹.loder = -f.loder

The logarithmic derivative of the inverse: loder(f⁻¹) = -loder(f). This is Corollary 7.8.16 (cor.fps.loder.inv).

Note: This does NOT require R to be a ℚ-algebra.

@[simp]

theorem PowerSeries.loder_one {R : Type u_2} [Field R] : loder 1 = 0

The logarithmic derivative of 1 is 0.

Section 7.10.2: Exp and Log for Infinite Products

The Exp and Log maps convert between infinite sums and products. These results require K to be a ℚ-algebra for the formal exp and log to be defined.

Propositions prop.fps.Exp-Log-infsum and prop.fps.Exp-Log-infprod state:

• Exp(∑_{i ∈ I} f_i) = ∏_{i ∈ I} Exp(f_i) for summable families in K⟦X⟧_0
• Log(∏_{i ∈ I} f_i) = ∑_{i ∈ I} Log(f_i) for multipliable families in K⟦X⟧_1

Summable families in K⟦X⟧₀

def PowerSeries.SummableFPS₀ {K : Type u_2} [CommRing K] {I : Type u_3} (f : I → ↑PowerSeries₀) : Prop

A family of FPS in K⟦X⟧₀ is summable if for each coefficient index n, only finitely many family members have nonzero n-th coefficient.

This is the notion of summability appropriate for K⟦X⟧₀.

Equations

• PowerSeries.SummableFPS₀ f = ∀ (n : ℕ), {i : I | (PowerSeries.coeff n) ↑(f i) ≠ 0}.Finite

theorem PowerSeries.SummableFPS₀.sum_mem {K : Type u_2} [CommRing K] {I : Type u_3} (f : I → ↑PowerSeries₀) (_hf : SummableFPS₀ f) : ∑ᶠ (i : I), ↑(f i) ∈ PowerSeries₀

For a summable family in K⟦X⟧₀, the sum is also in K⟦X⟧₀.

noncomputable def PowerSeries.summableFPS₀Sum {K : Type u_2} [CommRing K] {I : Type u_3} (f : I → ↑PowerSeries₀) (_hf : SummableFPS₀ f) : ↑PowerSeries₀

The coefficient-wise sum of a summable family in K⟦X⟧₀.

Important: This is defined coefficient-wise using mk, NOT using finsum on the entire power series. The reason is that finsum returns 0 when the support is infinite, but SummableFPS₀ only guarantees finite support for each coefficient, not for the entire family.

For each coefficient n, only finitely many terms contribute (by SummableFPS₀), so the finsum ∑ᶠ i, coeff n (f i).val is well-defined and equals a finite sum.

Equations

• PowerSeries.summableFPS₀Sum f _hf = ⟨PowerSeries.mk fun (n : ℕ) => ∑ᶠ (i : I), (PowerSeries.coeff n) ↑(f i), ⋯⟩

Multipliable families in K⟦X⟧₁

def PowerSeries.MultipliableFPS₁ {K : Type u_2} [CommRing K] {I : Type u_3} (f : I → ↑PowerSeries₁) : Prop

A family of FPS in K⟦X⟧₁ is multipliable if for each coefficient index n, the n-th coefficient of the product is finitely determined.

This is the notion of multipliability appropriate for K⟦X⟧₁.

Equations

• PowerSeries.MultipliableFPS₁ f = PowerSeries.Multipliable fun (i : I) => ↑(f i)

theorem PowerSeries.MultipliableFPS₁.prod_mem {K : Type u_2} [CommRing K] {I : Type u_3} (f : I → ↑PowerSeries₁) (hf : MultipliableFPS₁ f) : tprod (fun (i : I) => ↑(f i)) hf ∈ PowerSeries₁

For a multipliable family in K⟦X⟧₁, the product is also in K⟦X⟧₁.

noncomputable def PowerSeries.multipliableFPS₁Prod {K : Type u_2} [CommRing K] {I : Type u_3} (f : I → ↑PowerSeries₁) (hf : MultipliableFPS₁ f) : ↑PowerSeries₁

The product of a multipliable family in K⟦X⟧₁ as an element of K⟦X⟧₁.

Equations

• PowerSeries.multipliableFPS₁Prod f hf = ⟨PowerSeries.tprod (fun (i : I) => ↑(f i)) hf, ⋯⟩

The main theorem: Log converts products to sums

theorem PowerSeries.Log_summable_of_multipliable {K : Type u_2} [CommRing K] [Algebra ℚ K] {I : Type u_3} (f : I → ↑PowerSeries₁) (hf : MultipliableFPS₁ f) : SummableFPS₀ fun (i : I) => Log (f i)

If (f_i)_{i ∈ I} is a multipliable family in K⟦X⟧₁, then (Log f_i)_{i ∈ I} is a summable family in K⟦X⟧₀.

This is part of Proposition prop.fps.Exp-Log-infprod from the source material.

theorem PowerSeries.Log_tprod {K : Type u_2} [CommRing K] [Algebra ℚ K] {I : Type u_3} (f : I → ↑PowerSeries₁) (hf : MultipliableFPS₁ f) (hf_sum : SummableFPS₀ fun (i : I) => Log (f i) := ⋯) : Log (multipliableFPS₁Prod f hf) = summableFPS₀Sum (fun (i : I) => Log (f i)) hf_sum

Proposition prop.fps.Exp-Log-infprod: Log converts infinite products to infinite sums.

If (f_i)_{i ∈ I} is a multipliable family of FPSs in K⟦X⟧₁, then:

1. (Log f_i)_{i ∈ I} is a summable family of FPSs in K⟦X⟧₀
2. ∏_{i ∈ I} f_i ∈ K⟦X⟧₁
3. Log(∏_{i ∈ I} f_i) = ∑_{i ∈ I} Log(f_i)

This is the infinite version of Log_mul: Log(fg) = Log(f) + Log(g).

The proof strategy:

1. Use Log_mul for finite products
2. Show that for multipliable families, the finite partial products converge
3. Use continuity of Log (which follows from the coefficient-wise definition) to pass to the limit

theorem PowerSeries.Exp_multipliable_of_summable {K : Type u_2} [CommRing K] [Algebra ℚ K] {I : Type u_3} (g : I → ↑PowerSeries₀) (hg : SummableFPS₀ g) : MultipliableFPS₁ fun (i : I) => Exp (g i)

theorem PowerSeries.Exp_sum {K : Type u_2} [CommRing K] [Algebra ℚ K] {I : Type u_3} (g : I → ↑PowerSeries₀) (hg : SummableFPS₀ g) (hg_mul : MultipliableFPS₁ fun (i : I) => Exp (g i) := ⋯) : Exp (summableFPS₀Sum g hg) = multipliableFPS₁Prod (fun (i : I) => Exp (g i)) hg_mul

Exp converts infinite sums to infinite products.

This is the infinite version of Exp_add.