Commit 2023-06-15 20:07 33fd7e14

View on Github →

feat: port Algebra.ContinuedFractions.Computation.Approximations (#3917)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

added theorem GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_lt_one

added theorem GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_nonneg

added theorem GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_nonneg_lt_one

added theorem GeneralizedContinuedFraction.IntFractPair.one_le_succ_nth_stream_b

added theorem GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv

added theorem GeneralizedContinuedFraction.abs_sub_convergents_le'

added theorem GeneralizedContinuedFraction.abs_sub_convergents_le

added theorem GeneralizedContinuedFraction.determinant

added theorem GeneralizedContinuedFraction.determinant_aux

added theorem GeneralizedContinuedFraction.exists_int_eq_of_part_denom

added theorem GeneralizedContinuedFraction.fib_le_of_continuantsAux_b

added theorem GeneralizedContinuedFraction.le_of_succ_get?_denom

added theorem GeneralizedContinuedFraction.le_of_succ_succ_get?_continuantsAux_b

added theorem GeneralizedContinuedFraction.of_denom_mono

added theorem GeneralizedContinuedFraction.of_one_le_get?_part_denom

added theorem GeneralizedContinuedFraction.of_part_num_eq_one

added theorem GeneralizedContinuedFraction.of_part_num_eq_one_and_exists_int_part_denom_eq

added theorem GeneralizedContinuedFraction.sub_convergents_eq

added theorem GeneralizedContinuedFraction.succ_nth_fib_le_of_nth_denom

added theorem GeneralizedContinuedFraction.zero_le_of_continuantsAux_b

added theorem GeneralizedContinuedFraction.zero_le_of_denom