Euler continued fraction

This file formalizes a transformation on generalized continued fractions over a field K. It defines a map sending a generalized continued fraction to an equivalent Euler continued fraction obtained by an explicit transformation of its coefficient stream.

Main definitions

• GenContFract.IsEuler : predicate for a generalized continued fraction to be an Euler continued fraction.
• GenContFract.euler : constructs a generalized continued fraction from a head term h and a coefficient stream ρ.
• GenContFract.toEuler : transforms a generalized continued fraction to an Euler continued fraction.

Main results

• convs_euler : explicit formula for convergents of an Euler continued fraction.
• convs_toEuler : equivalence of convergents between a generalized continued fraction and its corresponding Euler continued fraction.

References

• https://en.wikipedia.org/wiki/Euler%27s_continued_fraction_formula
• Wall, H.S., Analytic Theory of Continued Fractions

def GenContFract.IsEuler {K : Type u_1} [Field K] (g : GenContFract K) : Prop

An Euler continued fraction is a generalized continued fraction of the form $$ h + \cfrac{\rho_0} {1 - \cfrac{\rho_1} {1 + \rho_1 - \cfrac{\rho_2} {1 + \rho_2 - \cfrac{\rho_3} {1 + \rho_3 - \dots}}}} $$

Equations

• g.IsEuler = ∀ (n : ℕ) (aₙ bₙ : K), g.s.get? n = some { a := aₙ, b := bₙ } → if n = 0 then bₙ = 1 else aₙ + bₙ = 1

def GenContFract.euler {K : Type u_1} [Field K] (h : K) (ρ : Stream'.Seq K) : GenContFract K

euler h ρ constructs an Euler continued fraction whose coefficients are obtained from the stream ρ with head term h.

Equations

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

def GenContFract.toEuler {K : Type u_1} [Field K] (g : GenContFract K) : GenContFract K

toEuler g is the Euler continued fraction equivalent to g, where ρ₀ = a₀ / b₀ and ρₙ = - aₙ * Bₙ₋₁ / Bₙ₊₁ for n > 0.

Equations

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

@[simp]

theorem GenContFract.terminatedAt_euler {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} : (euler h ρ).TerminatedAt n ↔ ρ.TerminatedAt n

theorem GenContFract.exists_euler_s_of_not_terminatedAt_zero {K : Type u_1} [Field K] {h : K} {ρ : Stream'.Seq K} (not_terminatedAt_zero : ¬ρ.TerminatedAt 0) : ∃ (a : K), (euler h ρ).s.get? 0 = some { a := a, b := 1 }

theorem GenContFract.exists_euler_s_of_not_terminatedAt_succ {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} (not_terminatedAt_n_succ : ¬ρ.TerminatedAt (n + 1)) : ∃ (a : K), (euler h ρ).s.get? (n + 1) = some { a := -a, b := 1 + a }

@[simp]

theorem GenContFract.isEuler_euler {K : Type u_1} [Field K] {h : K} {ρ : Stream'.Seq K} : (euler h ρ).IsEuler

theorem GenContFract.isEuler_iff_exists_euler {K : Type u_1} [Field K] {g : GenContFract K} : g.IsEuler ↔ ∃ (ρ : Stream'.Seq K), euler g.h ρ = g

@[simp]

theorem GenContFract.isEuler_toEuler {K : Type u_1} [Field K] {g : GenContFract K} : g.toEuler.IsEuler

@[simp]

theorem GenContFract.terminatedAt_toEuler {K : Type u_1} [Field K] {n : ℕ} {g : GenContFract K} : g.toEuler.TerminatedAt n ↔ g.TerminatedAt n

theorem GenContFract.euler_s_zero {K : Type u_1} [Field K] {h : K} {ρ : Stream'.Seq K} : (euler h ρ).s.get? 0 = Option.map (fun (ρ : K) => { a := ρ, b := 1 }) (ρ.get? 0)

theorem GenContFract.euler_s_succ {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} : (euler h ρ).s.get? (n + 1) = Option.map (fun (ρ : K) => { a := -ρ, b := 1 + ρ }) (ρ.get? (n + 1))

theorem GenContFract.toEuler_s_zero {K : Type u_1} [Field K] {g : GenContFract K} : g.toEuler.s.get? 0 = Option.map (fun (x : Pair K) => match x with | { a := a, b := b } => { a := a / b, b := 1 }) (g.s.get? 0)

theorem GenContFract.toEuler_s_succ {K : Type u_1} [Field K] {n : ℕ} {g : GenContFract K} : g.toEuler.s.get? (n + 1) = Option.map (fun (x : Pair K) => match x with | { a := a, b := b } => { a := a * g.dens n / g.dens (n + 2), b := 1 - a * g.dens n / g.dens (n + 2) }) (g.s.get? (n + 1))

@[simp]

theorem GenContFract.euler_h {K : Type u_1} [Field K] {h : K} {ρ : Stream'.Seq K} : (euler h ρ).h = h

@[simp]

theorem GenContFract.toEuler_h {K : Type u_1} [Field K] {g : GenContFract K} : g.toEuler.h = g.h

@[simp]

theorem GenContFract.partNum_euler_zero {K : Type u_1} [Field K] {h : K} {ρ : Stream'.Seq K} : (euler h ρ).partNums.get? 0 = ρ.get? 0

@[simp]

theorem GenContFract.partDen_euler_zero {K : Type u_1} [Field K] {h : K} {ρ : Stream'.Seq K} : (euler h ρ).partDens.get? 0 = Option.map (fun (x : K) => 1) (ρ.get? 0)

@[simp]

theorem GenContFract.partNum_euler_succ {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} : (euler h ρ).partNums.get? (n + 1) = Option.map (fun (x : K) => -x) (ρ.get? (n + 1))

@[simp]

theorem GenContFract.partDen_euler_succ {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} : (euler h ρ).partDens.get? (n + 1) = Option.map (fun (x : K) => 1 + x) (ρ.get? (n + 1))

@[simp]

theorem GenContFract.IsEuler.dens_eq_one {K : Type u_1} [Field K] {n : ℕ} {g : GenContFract K} (h : g.IsEuler) : g.dens n = 1

The denominators of an Euler continued fraction are all 1.

theorem GenContFract.nums_euler {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} : (euler h ρ).nums n = h + ∑ i ∈ Finset.range n, ∏ j ∈ Finset.range (i + 1), (ρ.get? j).getD 0

The numerators of an Euler continued fraction are given by the formula $$ A_n = h + \sum_{i = 0}^{n - 1} \prod_{j = 0}^i \rho_j $$

theorem GenContFract.convs_euler {K : Type u_1} [Field K] {n : ℕ} {h : K} {ρ : Stream'.Seq K} : (euler h ρ).convs n = h + ∑ i ∈ Finset.range n, ∏ j ∈ Finset.range (i + 1), (ρ.get? j).getD 0

Euler's continued fraction formula: the convergents of an Euler continued fraction are given by the formula $$ \dfrac{A_n}{B_n} = h + \sum_{i = 0}^{n - 1} \prod_{j = 0}^i \rho_j $$ for example:

• A₀ / B₀ = h
• A₁ / B₁ = h + ρ₀
• A₂ / B₂ = h + ρ₀ + ρ₀ * ρ₁
• Aₙ / Bₙ = h + ρ₀ + ρ₀ * ρ₁ + ρ₀ * ρ₁ * ρ₂ + ... + ρ₀ * ρ₁ * ρ₂ * ... * ρₙ₋₁

@[simp]

theorem GenContFract.IsEuler.toEuler {K : Type u_1} [Field K] {g : GenContFract K} (hg : g.IsEuler) : g.toEuler = g

The transformation toEuler is idempotent.

theorem GenContFract.convs_toEuler_of_forall_le {K : Type u_1} [Field K] {n : ℕ} {g : GenContFract K} (hB : ∀ m ≤ n, g.dens m ≠ 0) (m : ℕ) : m ≤ n → g.toEuler.convs m = g.convs m

theorem GenContFract.convs_toEuler {K : Type u_1} [Field K] {g : GenContFract K} (hB : ∀ (m : ℕ), g.dens m ≠ 0) : g.toEuler.convs = g.convs

The transformation toEuler preserves the convergents.

theorem GenContFract.convs_eq_sum_of_forall_le {K : Type u_1} [Field K] {n : ℕ} {g : GenContFract K} (hB : ∀ m ≤ n, g.dens m ≠ 0) : g.convs n = g.h + ∑ i ∈ Finset.range n, (-∏ j ∈ Finset.range (i + 1), -(g.partNums.get? j).getD 0) / (g.dens i * g.dens (i + 1))

theorem SimpContFract.convs_eq_sum_of_forall_le {K : Type u_1} [Field K] {n : ℕ} {s : SimpContFract K} (not_terminatedAt_n : ¬(↑s).TerminatedAt n) (hB : ∀ m ≤ n, (↑s).dens m ≠ 0) : (↑s).convs n = (↑s).h + ∑ i ∈ Finset.range n, (-1) ^ i / ((↑s).dens i * (↑s).dens (i + 1))