Logarithmic Power Series

This file defines the logarithmic power series log A = ∑ (-1)^(n+1)/n · Xⁿ over ℚ-algebras and establishes its key properties.

Main definitions

• PowerSeries.log: The power series log(1+X) = X - X²/2 + X³/3 - ⋯.

Main results

• PowerSeries.coeff_log: The coefficient of log A at n is (-1)^(n+1)/n for n ≥ 1, and 0 for n = 0.
• PowerSeries.constantCoeff_log: The constant term of log A is 0.
• PowerSeries.map_log: log is preserved by ring homomorphisms between ℚ-algebras.
• PowerSeries.coeff_one_log: The coefficient of log A at 1 is 1.
• PowerSeries.order_log: The order of log A is 1.
• PowerSeries.deriv_log: The derivative of log(1+X) is the geometric series ∑ (-1)^n · Xⁿ = 1/(1+X).

def PowerSeries.log (A : Type u_1) [CommRing A] [Algebra ℚ A] : PowerSeries A

Power series for log(1 + X) = X - X²/2 + X³/3 - ⋯.

Equations

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

@[simp]

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

@[simp]

theorem PowerSeries.constantCoeff_log {A : Type u_1} [CommRing A] [Algebra ℚ A] : constantCoeff (log A) = 0

@[simp]

theorem PowerSeries.map_log {A : Type u_1} [CommRing A] [Algebra ℚ A] {A' : Type u_2} [CommRing A'] [Algebra ℚ A'] (f : A →+* A') : (map f) (log A) = log A'

theorem PowerSeries.coeff_one_log {A : Type u_1} [CommRing A] [Algebra ℚ A] : (coeff 1) (log A) = 1

theorem PowerSeries.order_log {A : Type u_1} [CommRing A] [Algebra ℚ A] [Nontrivial A] : (log A).order = 1

theorem PowerSeries.deriv_log {A : Type u_1} [CommRing A] [Algebra ℚ A] : (derivative A) (log A) = mk fun (n : ℕ) => (algebraMap ℚ A) ((-1) ^ n)

The derivative of log(1+X) is the geometric series 1 - X + X² - X³ + ⋯ = 1/(1+X).

Substitution

theorem PowerSeries.HasSubst.log {A : Type u_1} [CommRing A] [Algebra ℚ A] : HasSubst (PowerSeries.log A)

theorem PowerSeries.HasSubst.exp_sub_one {A : Type u_1} [CommRing A] [Algebra ℚ A] : HasSubst (exp A - 1)

noncomputable def PowerSeries.logOf {A : Type u_1} [CommRing A] [Algebra ℚ A] (f : PowerSeries A) : PowerSeries A

logOf f is log(1+X) substituted at f - 1, i.e., (f-1) - (f-1)²/2 + (f-1)³/3 - ⋯.

Equations

• f.logOf = PowerSeries.subst (f - 1) (PowerSeries.log A)

theorem PowerSeries.logOf_eq {A : Type u_1} [CommRing A] [Algebra ℚ A] (f : PowerSeries A) : f.logOf = subst (f - 1) (log A)

theorem PowerSeries.constantCoeff_logOf {A : Type u_1} [CommRing A] [Algebra ℚ A] {f : PowerSeries A} (hf : constantCoeff f = 1) : constantCoeff f.logOf = 0

@[simp]

theorem PowerSeries.logOf_one_add_X (A : Type u_1) [CommRing A] [Algebra ℚ A] : (1 + X).logOf = log A