def Hex.TSeries.logUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (m : Nat) (a : TSeries R n) : TSeries R n

Formal logarithm computed only below precision m.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TSeries.log {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) : TSeries R n

Formal logarithm with zero constant coefficient.

Equations

• a.log = Hex.TSeries.logUpTo n a

def Hex.TSeries.expStep {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a y : TSeries R n) (m : Nat) : TSeries R n

One bounded exponential Newton update.

Equations

• a.expStep y m = Hex.TSeries.mulUpTo m y (Hex.TSeries.C 1 + a - Hex.TSeries.logUpTo m y)

def Hex.TSeries.expUpTo {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (m : Nat) (a : TSeries R n) : TSeries R n

Formal exponential computed only below precision m.

Equations

• Hex.TSeries.expUpTo m a = Hex.TSeries.ofFn fun (i : Nat) => if i < m then (Hex.TSeries.newton a.expStep 1 (Hex.TSeries.steps (min m n))).coeff i else 0

def Hex.TSeries.exp {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) : TSeries R n

Formal exponential with constant coefficient one.

Equations

• a.exp = Hex.TSeries.expUpTo n a

theorem Hex.TSeries.deriv_log {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) (_h : (a - 1).coeff 0 = 0) : a.log.deriv = a.deriv * (a.invOfUnit 1).truncate (n - 1) ⋯

The derivative characterizes the logarithm. The constant-term hypothesis is retained as the public domain contract shared by the other logarithm laws; the derivative identity itself follows from the total implementation without using it.

theorem Hex.TSeries.log_coeff_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) (_h : (a - 1).coeff 0 = 0) (h0 : 0 < n) : a.log.coeff 0 = 0

The logarithm has zero constant coefficient at positive precision. The constant-term hypothesis is retained for a stable, uniform logarithm API even though this particular coefficient identity does not use it.

theorem Hex.TSeries.exp_coeff_zero {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) (h : a.coeff 0 = 0) (h0 : 0 < n) : a.exp.coeff 0 = 1

The exponential has constant coefficient one at positive precision.

theorem Hex.TSeries.logUpTo_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (m : Nat) (a : TSeries R n) (ha : (a - 1).coeff 0 = 0) : Agree m (logUpTo m a) a.log

Bounded logarithm agrees with the full logarithm throughout the requested prefix.

theorem Hex.TSeries.expUpTo_agree {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (m : Nat) (a : TSeries R n) (ha : a.coeff 0 = 0) : Agree m (expUpTo m a) a.exp

Bounded exponential agrees with the full exponential throughout the requested prefix.

theorem Hex.TSeries.log_exp {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) (h : a.coeff 0 = 0) : a.exp.log = a

Logarithm is a left inverse to exponential on zero-constant series.

theorem Hex.TSeries.exp_log {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a : TSeries R n) (h : (a - 1).coeff 0 = 0) : a.log.exp = a

Exponential is a left inverse to logarithm on one-constant series.

theorem Hex.TSeries.exp_add {R : Type u} {n : Nat} [Lean.Grind.CommRing R] [NatInverses R (n - 1)] (a b : TSeries R n) (ha : a.coeff 0 = 0) (hb : b.coeff 0 = 0) : (a + b).exp = a.exp * b.exp

Exponential carries addition to multiplication.