diff --git a/Mathlib.lean b/Mathlib.lean index f6b6f903c32aa1..33b56ac9ce43b6 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -52,6 +52,7 @@ import Mathlib.Algebra.CharZero.Infinite import Mathlib.Algebra.CharZero.Lemmas import Mathlib.Algebra.CharZero.Quotient import Mathlib.Algebra.ContinuedFractions.Basic +import Mathlib.Algebra.ContinuedFractions.Translations import Mathlib.Algebra.CovariantAndContravariant import Mathlib.Algebra.CubicDiscriminant import Mathlib.Algebra.DirectSum.Basic diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean new file mode 100644 index 00000000000000..7d8243cc059bac --- /dev/null +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -0,0 +1,192 @@ +/- +Copyright (c) 2019 Kevin Kappelmann. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Kappelmann + +! This file was ported from Lean 3 source module algebra.continued_fractions.translations +! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Algebra.ContinuedFractions.Basic + +/-! +# Basic Translation Lemmas Between Functions Defined for Continued Fractions + +## Summary + +Some simple translation lemmas between the different definitions of functions defined in +`Algebra.ContinuedFractions.Basic`. +-/ + + +namespace GeneralizedContinuedFraction + +section General + +/-! +### Translations Between General Access Functions + +Here we give some basic translations that hold by definition between the various methods that allow +us to access the numerators and denominators of a continued fraction. +-/ + + +variable {α : Type _} {g : GeneralizedContinuedFraction α} {n : ℕ} + +theorem terminatedAt_iff_s_terminatedAt : g.TerminatedAt n ↔ g.s.TerminatedAt n := by rfl +#align generalized_continued_fraction.terminated_at_iff_s_terminated_at GeneralizedContinuedFraction.terminatedAt_iff_s_terminatedAt + +theorem terminatedAt_iff_s_none : g.TerminatedAt n ↔ g.s.get? n = none := by rfl +#align generalized_continued_fraction.terminated_at_iff_s_none GeneralizedContinuedFraction.terminatedAt_iff_s_none + +theorem part_num_none_iff_s_none : g.partialNumerators.get? n = none ↔ g.s.get? n = none := by + cases s_nth_eq : g.s.get? n <;> simp [partialNumerators, s_nth_eq] +#align generalized_continued_fraction.part_num_none_iff_s_none GeneralizedContinuedFraction.part_num_none_iff_s_none + +theorem terminatedAt_iff_part_num_none : g.TerminatedAt n ↔ g.partialNumerators.get? n = none := by + rw [terminatedAt_iff_s_none, part_num_none_iff_s_none] +#align generalized_continued_fraction.terminated_at_iff_part_num_none GeneralizedContinuedFraction.terminatedAt_iff_part_num_none + +theorem part_denom_none_iff_s_none : g.partialDenominators.get? n = none ↔ g.s.get? n = none := by + cases s_nth_eq : g.s.get? n <;> simp [partialDenominators, s_nth_eq] +#align generalized_continued_fraction.part_denom_none_iff_s_none GeneralizedContinuedFraction.part_denom_none_iff_s_none + +theorem terminatedAt_iff_part_denom_none : g.TerminatedAt n ↔ g.partialDenominators.get? n = none := + by rw [terminatedAt_iff_s_none, part_denom_none_iff_s_none] +#align generalized_continued_fraction.terminated_at_iff_part_denom_none GeneralizedContinuedFraction.terminatedAt_iff_part_denom_none + +theorem part_num_eq_s_a {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : + g.partialNumerators.get? n = some gp.a := by simp [partialNumerators, s_nth_eq] +#align generalized_continued_fraction.part_num_eq_s_a GeneralizedContinuedFraction.part_num_eq_s_a + +theorem part_denom_eq_s_b {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : + g.partialDenominators.get? n = some gp.b := by simp [partialDenominators, s_nth_eq] +#align generalized_continued_fraction.part_denom_eq_s_b GeneralizedContinuedFraction.part_denom_eq_s_b + +theorem exists_s_a_of_part_num {a : α} (nth_part_num_eq : g.partialNumerators.get? n = some a) : + ∃ gp, g.s.get? n = some gp ∧ gp.a = a := by + simpa [partialNumerators, Stream'.Seq.map_get?] using nth_part_num_eq +#align generalized_continued_fraction.exists_s_a_of_part_num GeneralizedContinuedFraction.exists_s_a_of_part_num + +theorem exists_s_b_of_part_denom {b : α} + (nth_part_denom_eq : g.partialDenominators.get? n = some b) : + ∃ gp, g.s.get? n = some gp ∧ gp.b = b := by + simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq +#align generalized_continued_fraction.exists_s_b_of_part_denom GeneralizedContinuedFraction.exists_s_b_of_part_denom + +end General + +section WithDivisionRing + +/-! +### Translations Between Computational Functions + +Here we give some basic translations that hold by definition for the computational methods of a +continued fraction. +-/ + + +variable {K : Type _} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] + +theorem nth_cont_eq_succ_nth_cont_aux : g.continuants n = g.continuantsAux (n + 1) := + rfl +#align generalized_continued_fraction.nth_cont_eq_succ_nth_cont_aux GeneralizedContinuedFraction.nth_cont_eq_succ_nth_cont_aux + +theorem num_eq_conts_a : g.numerators n = (g.continuants n).a := + rfl +#align generalized_continued_fraction.num_eq_conts_a GeneralizedContinuedFraction.num_eq_conts_a + +theorem denom_eq_conts_b : g.denominators n = (g.continuants n).b := + rfl +#align generalized_continued_fraction.denom_eq_conts_b GeneralizedContinuedFraction.denom_eq_conts_b + +theorem convergent_eq_num_div_denom : g.convergents n = g.numerators n / g.denominators n := + rfl +#align generalized_continued_fraction.convergent_eq_num_div_denom GeneralizedContinuedFraction.convergent_eq_num_div_denom + +theorem convergent_eq_conts_a_div_conts_b : + g.convergents n = (g.continuants n).a / (g.continuants n).b := + rfl +#align generalized_continued_fraction.convergent_eq_conts_a_div_conts_b GeneralizedContinuedFraction.convergent_eq_conts_a_div_conts_b + +theorem exists_conts_a_of_num {A : K} (nth_num_eq : g.numerators n = A) : + ∃ conts, g.continuants n = conts ∧ conts.a = A := by simpa +#align generalized_continued_fraction.exists_conts_a_of_num GeneralizedContinuedFraction.exists_conts_a_of_num + +theorem exists_conts_b_of_denom {B : K} (nth_denom_eq : g.denominators n = B) : + ∃ conts, g.continuants n = conts ∧ conts.b = B := by simpa +#align generalized_continued_fraction.exists_conts_b_of_denom GeneralizedContinuedFraction.exists_conts_b_of_denom + +@[simp] +theorem zeroth_continuant_aux_eq_one_zero : g.continuantsAux 0 = ⟨1, 0⟩ := + rfl +#align generalized_continued_fraction.zeroth_continuant_aux_eq_one_zero GeneralizedContinuedFraction.zeroth_continuant_aux_eq_one_zero + +@[simp] +theorem first_continuant_aux_eq_h_one : g.continuantsAux 1 = ⟨g.h, 1⟩ := + rfl +#align generalized_continued_fraction.first_continuant_aux_eq_h_one GeneralizedContinuedFraction.first_continuant_aux_eq_h_one + +@[simp] +theorem zeroth_continuant_eq_h_one : g.continuants 0 = ⟨g.h, 1⟩ := + rfl +#align generalized_continued_fraction.zeroth_continuant_eq_h_one GeneralizedContinuedFraction.zeroth_continuant_eq_h_one + +@[simp] +theorem zeroth_numerator_eq_h : g.numerators 0 = g.h := + rfl +#align generalized_continued_fraction.zeroth_numerator_eq_h GeneralizedContinuedFraction.zeroth_numerator_eq_h + +@[simp] +theorem zeroth_denominator_eq_one : g.denominators 0 = 1 := + rfl +#align generalized_continued_fraction.zeroth_denominator_eq_one GeneralizedContinuedFraction.zeroth_denominator_eq_one + +@[simp] +theorem zeroth_convergent_eq_h : g.convergents 0 = g.h := by + simp [convergent_eq_num_div_denom, num_eq_conts_a, denom_eq_conts_b, div_one] +#align generalized_continued_fraction.zeroth_convergent_eq_h GeneralizedContinuedFraction.zeroth_convergent_eq_h + +theorem second_continuant_aux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.continuantsAux 2 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by + simp [zeroth_s_eq, continuantsAux, nextContinuants, nextDenominator, nextNumerator] +#align generalized_continued_fraction.second_continuant_aux_eq GeneralizedContinuedFraction.second_continuant_aux_eq + +theorem first_continuant_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.continuants 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by + simp [nth_cont_eq_succ_nth_cont_aux] + -- porting note: simp used to work here, but now it can't figure out that 1 + 1 = 2 + convert second_continuant_aux_eq zeroth_s_eq +#align generalized_continued_fraction.first_continuant_eq GeneralizedContinuedFraction.first_continuant_eq + +theorem first_numerator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.numerators 1 = gp.b * g.h + gp.a := by simp [num_eq_conts_a, first_continuant_eq zeroth_s_eq] +#align generalized_continued_fraction.first_numerator_eq GeneralizedContinuedFraction.first_numerator_eq + +theorem first_denominator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.denominators 1 = gp.b := by simp [denom_eq_conts_b, first_continuant_eq zeroth_s_eq] +#align generalized_continued_fraction.first_denominator_eq GeneralizedContinuedFraction.first_denominator_eq + +@[simp] +theorem zeroth_convergent'_aux_eq_zero {s : Stream'.Seq <| Pair K} : + convergents'Aux s 0 = (0 : K) := + rfl +#align generalized_continued_fraction.zeroth_convergent'_aux_eq_zero GeneralizedContinuedFraction.zeroth_convergent'_aux_eq_zero + +@[simp] +theorem zeroth_convergent'_eq_h : g.convergents' 0 = g.h := by simp [convergents'] +#align generalized_continued_fraction.zeroth_convergent'_eq_h GeneralizedContinuedFraction.zeroth_convergent'_eq_h + +theorem convergents'Aux_succ_none {s : Stream'.Seq (Pair K)} (h : s.head = none) (n : ℕ) : + convergents'Aux s (n + 1) = 0 := by simp [convergents'Aux, h, convergents'Aux.match_1] +#align generalized_continued_fraction.convergents'_aux_succ_none GeneralizedContinuedFraction.convergents'Aux_succ_none + +theorem convergents'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p) + (n : ℕ) : convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux s.tail n) := by + simp [convergents'Aux, h, convergents'Aux.match_1] +#align generalized_continued_fraction.convergents'_aux_succ_some GeneralizedContinuedFraction.convergents'Aux_succ_some + +end WithDivisionRing + +end GeneralizedContinuedFraction