English
The nth convergent of GenContFract.of ξ equals ξ.convergent n (cast).
Русский
N-й конвергент GenContFract.of ξ равен ξ.convergent n (с приведением типов).
LaTeX
$$$$ (\\mathrm{GenContFract}.of \\xi).convs n = \\xi.convergent n.$$$$
Lean4
/-- The technical version of *Legendre's Theorem*. -/
theorem exists_rat_eq_convergent' {v : ℕ} (h : ContfracLegendre.Ass ξ u v) : ∃ n, (u / v : ℚ) = ξ.convergent n :=
by
induction v using Nat.strong_induction_on generalizing ξ u with
| h v ih => ?_
rcases lt_trichotomy v 1 with (ht | rfl | ht)
· replace h := h.2.2
simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul, cast_zero, inv_zero] at h
exact False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)
· rw [Nat.cast_one, div_one]
obtain ⟨_, h₁, h₂⟩ := h
rcases le_or_gt (u : ℝ) ξ with ht | ht
· use 0
rw [convergent_zero, Rat.coe_int_inj, eq_comm, floor_eq_iff]
convert And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2) <;> norm_num
· replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
have hξ₁ : ⌊ξ⌋ = u - 1 := by
rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ
· rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)
· have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 :=
by
rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one, one_add_one_eq_two,
inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
refine ⟨(fract_lt_one ξ).le, ?_⟩
rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
convert h₁ using 1
rw [sub_eq_add_neg]
norm_num
use 1
simp [convergent, hξ₁, hξ₂, cast_sub, cast_one]
· obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h
have Hv : (v : ℚ) ≠ 0 := (Nat.cast_pos.mpr (zero_lt_one.trans ht)).ne'
have huv₁' : (u - ⌊ξ⌋ * v).toNat < v := by zify; rwa [toNat_of_nonneg huv₀.le]
have inv : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * ↑v).toNat :=
(toNat_of_nonneg huv₀.le).symm ▸ invariant (Nat.cast_le.mpr ht) h
obtain ⟨n, hn⟩ := ih (u - ⌊ξ⌋ * v).toNat huv₁' inv
use n + 1
rw [convergent_succ, ← hn, (mod_cast toNat_of_nonneg huv₀.le : ((u - ⌊ξ⌋ * v).toNat : ℚ) = u - ⌊ξ⌋ * v),
cast_natCast, inv_div, sub_div, mul_div_cancel_right₀ _ Hv, add_sub_cancel]
