exists_gcf_pair_rat_eq_of_nth_contsAux

English

For any v and n, there exists a pair conts of rationals such that (of v).contsAux n equals conts.map (↑).

Русский

Для любого v и n существует пара рациональных conts такая, что (of v).contsAux n = conts.map (↑).

LaTeX

$$$\\exists conts : Pair\\ mathbb{Q},\\ (of\\, v).contsAux n = conts.map (\\uparrow)$$$

Lean4

nonrec theorem exists_gcf_pair_rat_eq_of_nth_contsAux :
    ∃ conts : Pair ℚ, (of v).contsAux n = (conts.map (↑) : Pair K) :=
  Nat.strong_induction_on n
    (by
      clear n
      let g := of v
      intro n IH
      rcases n with
        (_ | _ | n)
          -- n = 0

      · suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]
        use Pair.mk 1 0
        simp
          -- n = 1

      · suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [contsAux]
        use Pair.mk ⌊v⌋ 1
        simp [g]
          -- 2 ≤ n

      · obtain ⟨pred_conts, pred_conts_eq⟩ :=
          IH (n + 1) <|
            lt_add_one
              (n + 1)
                -- invoke the IH

        rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n
        · use pred_conts
          have : g.contsAux (n + 2) = g.contsAux (n + 1) := contsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
          simp only [g, this, pred_conts_eq]
            -- option.some

        · -- invoke the IH a second time

          obtain ⟨ppred_conts, ppred_conts_eq⟩ := IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1
          obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K) :=
            of_partNum_eq_one_and_exists_int_partDen_eq s_ppred_nth_eq
          simp only [g, a_eq_one, b_eq_z, contsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
          use nextConts 1 (z : ℚ) ppred_conts pred_conts
          cases ppred_conts; cases pred_conts
          simp [nextConts, nextNum, nextDen])

Похожие утверждения