-- Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean
theorem of_convergence_epsilon :
    ∀ ε > (0 : K), ∃ N : ℕ, ∀ n ≥ N, |v - (of v).convs n| < ε

Proof state:
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
⊢ |v - (of v).convs n| < ε

Tactic:
have : v = g.convs n := of_correctness_of_terminatedAt terminatedAt_n

Result:
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this : v = g.convs n
⊢ |v - (of v).convs n| < ε

Proof state:
case intro.inr.h
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ↑N' ≤ B * nB

Tactic:
calc
  (N' : K) ≤ (N : K) := by exact_mod_cast le_max_left _ _
  _ ≤ n := by exact_mod_cast n_ge_N
  _ ≤ fib n := by exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
  _ ≤ fib (n + 1) := by exact_mod_cast fib_le_fib_succ
  _ ≤ fib (n + 1) * fib (n + 1) := by exact_mod_cast (fib (n + 1)).le_mul_self
  _ ≤ fib (n + 1) * fib (n + 2) := by gcongr; exact_mod_cast fib_le_fib_succ
  _ ≤ B * nB := by gcongr

Result:
no goals

Proof state:
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
⊢ 1 / (B * nB) < ε

Tactic:
have B_ineq : (fib (n + 1) : K) ≤ B :=
  haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminatedAt_n
  succ_nth_fib_le_of_nth_den (Or.inr this)

Result:
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 1 / (B * nB) < ε

Proof state:
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
rcases (exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩

Result:
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
⊢ ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε

Proof state:
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ↑(fib n) ≤ ↑(fib (n + 1))

Tactic:
exact_mod_cast fib_le_fib_succ

Result:
no goals

Proof state:
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 1 / (B * nB) < ε

Tactic:
have zero_lt_B : 0 < B := B_ineq.trans_lt' <| mod_cast fib_pos.2 n.succ_pos

Result:
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 1 / (B * nB) < ε

Proof state:
case h.h
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ fib (n + 1) ≤ fib (n + 2)

Tactic:
exact_mod_cast fib_le_fib_succ

Result:
no goals

Proof state:
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this✝ : v = g.convs n
this : v - g.convs n = 0
⊢ |v - (of v).convs n| < ε

Tactic:
rw [this]

Result:
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this✝ : v = g.convs n
this : v - g.convs n = 0
⊢ |0| < ε

Proof state:
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * (B * nB)

Tactic:
calc 1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'
  _ ≤ ε * (B * nB) := ?_

Result:
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ε * ↑N' ≤ ε * (B * nB)

Proof state:
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
⊢ ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
let N := max N' 5

Result:
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := N' ⊔ 5
⊢ ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε