Commit 2023-06-16 10:41 851314e3

View on Github →

feat: port NumberTheory.DiophantineApproximation (#5126)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/DiophantineApproximation.lean

added theorem Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq

added theorem Rat.finite_rat_abs_sub_lt_one_div_den_sq

added def Real.ContfracLegendre.Ass

added theorem Real.continued_fraction_convergent_eq_convergent

added theorem Real.convergent_of_int

added theorem Real.convergent_of_zero

added theorem Real.convergent_succ

added theorem Real.convergent_zero

added theorem Real.exists_continued_fraction_convergent_eq_rat

added theorem Real.exists_int_int_abs_mul_sub_le

added theorem Real.exists_nat_abs_mul_sub_round_le

added theorem Real.exists_rat_abs_sub_le_and_den_le

added theorem Real.exists_rat_abs_sub_lt_and_lt_of_irrational

added theorem Real.exists_rat_eq_convergent'

added theorem Real.exists_rat_eq_convergent

added theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational

added theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational