Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-07 09:59 12c2acb8

View on Github →

feat(algebra/continued_fractions): add first set of approximation lemmas (#3218)

Estimated changes

Created src/algebra/continued_fractions/computation/approximations.lean

added theorem generalized_continued_fraction.exists_int_eq_of_part_denom

added theorem generalized_continued_fraction.fib_le_of_continuants_aux_b

added theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_lt_one

added theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_nonneg

added theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_nonneg_lt_one

added theorem generalized_continued_fraction.int_fract_pair.one_le_succ_nth_stream_b

added theorem generalized_continued_fraction.int_fract_pair.succ_nth_stream_b_le_nth_stream_fr_inv

added theorem generalized_continued_fraction.le_of_succ_nth_denom

added theorem generalized_continued_fraction.le_of_succ_succ_nth_continuants_aux_b

added theorem generalized_continued_fraction.of_denom_mono

added theorem generalized_continued_fraction.of_one_le_nth_part_denom

added theorem generalized_continued_fraction.of_part_num_eq_one

added theorem generalized_continued_fraction.of_part_num_eq_one_and_exists_int_part_denom_eq

added theorem generalized_continued_fraction.succ_nth_fib_le_of_nth_denom

added theorem generalized_continued_fraction.zero_le_of_continuants_aux_b

added theorem generalized_continued_fraction.zero_le_of_denom

Modified src/algebra/continued_fractions/computation/correctness_terminating.lean

deleted theorem generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_none

added theorem generalized_continued_fraction.of_correctness_of_nth_stream_eq_none

Modified src/algebra/continued_fractions/computation/translations.lean

added theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_fr_zero

added theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_gcf_of_nth_eq_some

deleted theorem generalized_continued_fraction.int_fract_pair.obtain_succ_nth_stream_of_fr_zero

deleted theorem generalized_continued_fraction.int_fract_pair.obtain_succ_nth_stream_of_gcf_of_nth_eq_some

Modified src/algebra/continued_fractions/continuants_recurrence.lean

Modified src/algebra/continued_fractions/convergents_equiv.lean

Modified src/algebra/continued_fractions/terminated_stable.lean

Modified src/algebra/continued_fractions/translations.lean

added theorem generalized_continued_fraction.exists_conts_a_of_num

added theorem generalized_continued_fraction.exists_conts_b_of_denom

added theorem generalized_continued_fraction.exists_s_a_of_part_num

added theorem generalized_continued_fraction.exists_s_b_of_part_denom

added theorem generalized_continued_fraction.first_continuant_eq

added theorem generalized_continued_fraction.first_denominator_eq

added theorem generalized_continued_fraction.first_numerator_eq

deleted theorem generalized_continued_fraction.obtain_conts_a_of_num

deleted theorem generalized_continued_fraction.obtain_conts_b_of_denom

deleted theorem generalized_continued_fraction.obtain_s_a_of_part_num

deleted theorem generalized_continued_fraction.obtain_s_b_of_part_denom

added theorem generalized_continued_fraction.second_continuant_aux_eq

added theorem generalized_continued_fraction.zeroth_denominator_eq_one

added theorem generalized_continued_fraction.zeroth_numerator_eq_h