English
For non-integer v (fract v ≠ 0), the (n+1)th term of the stream is the same as the nth term of the stream of the inverse fractional part: IntFractPair.stream v (n+1) = IntFractPair.stream (fract v)^{-1} n.
Русский
Для нецелого v (fract v ≠ 0) (n+1)-й член потока равен n-м члену потока для обратной дробной части: IntFractPair.stream v (n+1) = IntFractPair.stream (fract v)^{-1} n.
LaTeX
$$$\text{If } \operatorname{fract}(v) \neq 0,\; \operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \operatorname{IntFractPair}.\operatorname{stream}( (\operatorname{fract}(v))^{-1}, n)$$$
Lean4
/-- A recurrence relation that expresses the `(n+1)`th term of the stream of `IntFractPair`s
of `v` for non-integer `v` in terms of the `n`th term of the stream associated to
the inverse of the fractional part of `v`.
-/
theorem stream_succ (h : Int.fract v ≠ 0) (n : ℕ) :
IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n := by
induction n with
| zero =>
have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.of]
rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]
| succ n ih =>
rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome
· rw [hnone] at ih
rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone), succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
· obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
rw [hp] at ih
rcases eq_or_ne p.fr 0 with hz | hnz
· rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
· rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
