English
The continued fraction of v is defined as ContFract.of v = ⟨SimpContFract.of v, SimpContFract.of_isContFract v⟩.
Русский
Продолженная дробь числа v задаётся как ContFract.of v = ⟨SimpContFract.of v, SimpContFract.of_isContFract v⟩.
LaTeX
$$$\\\\text{ContFract.of}(v) = \\\\langle SimpContFract.of(v), SimpContFract.of_isContFract(v) \\\\rangle$$$
Lean4
/-- Shows that the sequence of denominators is monotone, that is `Bₙ ≤ Bₙ₊₁`. -/
theorem of_den_mono : (of v).dens n ≤ (of v).dens (n + 1) :=
by
let g := of v
rcases Decidable.em <| g.partDens.TerminatedAt n with terminated | not_terminated
· have : g.partDens.get? n = none := by rwa [Stream'.Seq.TerminatedAt] at terminated
have : g.TerminatedAt n := terminatedAt_iff_partDen_none.2 (by rwa [Stream'.Seq.TerminatedAt] at terminated)
have : g.dens (n + 1) = g.dens n := dens_stable_of_terminated n.le_succ this
rw [this]
· obtain ⟨b, nth_partDen_eq⟩ : ∃ b, g.partDens.get? n = some b := Option.ne_none_iff_exists'.mp not_terminated
have : 1 ≤ b := of_one_le_get?_partDen nth_partDen_eq
calc
g.dens n ≤ b * g.dens n := by simpa using mul_le_mul_of_nonneg_right this zero_le_of_den
_ ≤ g.dens (n + 1) := le_of_succ_get?_den nth_partDen_eq
