Continuants in a noncommutative ring

Euler's continuant K in a (noncommutative) ring and the absorption identities behind the Dubrovin–Gräter–Hanke strata: a⁻¹ + r + b⁻¹ = a⁻¹ K(a,r,b) b⁻¹.

Main results

• K with K [] = 1, K [x] = x, K (xs ++ [y, z]) = K (xs ++ [y]) * z + K xs; K_three: K [a, r, b] = a*r*b + a + b.
• absorb, absorb_K: absorption for units a, b; reduce_bilateral: two-sided reduction.
• harmonic_three: the harmonic denominator in a field.
• E_mul_three: the continuant is the (0,0) entry of E a * E r * E b in M₂(R), E x = !![x, 1; 1, 0] (the Möbius / GL₂ picture).

def Continuant.Kr {R : Type u_1} [Ring R] : List R → R

Continuant on the REVERSED list: Kr (xₙ :: xₙ₋₁ :: t) = Kr (xₙ₋₁ :: t) * xₙ + Kr t.

Equations

• Continuant.Kr [] = 1
• Continuant.Kr [x_1] = x_1
• Continuant.Kr (x_1 :: y :: t) = Continuant.Kr (y :: t) * x_1 + Continuant.Kr t

def Continuant.K {R : Type u_1} [Ring R] (l : List R) : R

Euler's continuant K(x₁, …, xₙ).

Equations

• Continuant.K l = Continuant.Kr l.reverse

@[simp]

theorem Continuant.K_nil {R : Type u_1} [Ring R] : K [] = 1

@[simp]

theorem Continuant.K_singleton {R : Type u_1} [Ring R] (x : R) : K [x] = x

theorem Continuant.K_append_two {R : Type u_1} [Ring R] (xs : List R) (y z : R) : K (xs ++ [y, z]) = K (xs ++ [y]) * z + K xs

Recursion K(x₁..xₙ y z) = K(x₁..xₙ y) * z + K(x₁..xₙ).

theorem Continuant.K_three {R : Type u_1} [Ring R] (a r b : R) : K [a, r, b] = a * r * b + a + b

(1) K [a, r, b] = a*r*b + a + b.

theorem Continuant.absorb {R : Type u_1} [Ring R] (a b : Rˣ) (r : R) : ↑a⁻¹ + r + ↑b⁻¹ = ↑a⁻¹ * (↑a * r * ↑b + ↑a + ↑b) * ↑b⁻¹

(2) Absorption: a⁻¹ + r + b⁻¹ = a⁻¹ (a r b + a + b) b⁻¹ for units a, b.

theorem Continuant.absorb_K {R : Type u_1} [Ring R] (a b : Rˣ) (r : R) : ↑a⁻¹ + r + ↑b⁻¹ = ↑a⁻¹ * K [↑a, r, ↑b] * ↑b⁻¹

(2') Absorption written with the continuant.

theorem Continuant.reduce_bilateral {R : Type u_1} [Ring R] (w₁ w₂ : Rˣ) (p s : R) : p + ↑w₁⁻¹ + ↑w₂⁻¹ + s = ↑w₁⁻¹ * (↑w₁ + ↑w₂ + ↑w₁ * (p + s) * ↑w₂) * ↑w₂⁻¹

(3) Two-sided reduction: p + w₁⁻¹ + w₂⁻¹ + s = w₁⁻¹ (w₁ + w₂ + w₁ (p + s) w₂) w₂⁻¹.

def Continuant.E {R : Type u_1} [Ring R] (x : R) : Matrix (Fin 2) (Fin 2) R

The GL₂ generator E x = !![x, 1; 1, 0].

Equations

• Continuant.E x = !![x, 1; 1, 0]

theorem Continuant.E_mul_three {R : Type u_1} [Ring R] (a r b : R) : E a * E r * E b = !![a * r * b + a + b, a * r + 1; r * b + 1, r]

(5) E a * E r * E b = !![a r b + a + b, a r + 1; r b + 1, r].

theorem Continuant.E_mul_three_00 {R : Type u_1} [Ring R] (a r b : R) : (E a * E r * E b) 0 0 = K [a, r, b]

theorem Continuant.E_mul_three_01 {R : Type u_1} [Ring R] (a r b : R) : (E a * E r * E b) 0 1 = a * r + 1

theorem Continuant.E_mul_three_10 {R : Type u_1} [Ring R] (a r b : R) : (E a * E r * E b) 1 0 = r * b + 1

theorem Continuant.E_mul_three_11 {R : Type u_1} [Ring R] (a r b : R) : (E a * E r * E b) 1 1 = r

theorem Continuant.harmonic_three {F : Type u_1} [Field F] (a b c : F) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (_h : a * b + b * c + c * a ≠ 0) : (1 / a + 1 / b + 1 / c)⁻¹ = a * b * c / (a * b + b * c + c * a)

(4) Harmonic denominator (commutative): (1/a + 1/b + 1/c)⁻¹ = abc/(ab+bc+ca).