Commit 2022-07-27 19:44 594e8848

View on Github →

feat(combinatorics/additive/behrend): Behrend's lower bound on Roth numbers (#15327) This proves the explicit bound on Roth's numbers of the form n / exp (O (sqrt (log n))).

Estimated changes

Modified src/algebra/order/floor.lean

modified theorem int.ceil_pos

added theorem nat.ceil_pos

Modified src/analysis/special_functions/pow.lean

added theorem real.exp_one_rpow

Modified src/combinatorics/additive/behrend.lean

added theorem behrend.bound

added theorem behrend.bound_aux'

added theorem behrend.bound_aux

added theorem behrend.ceil_lt_mul

added theorem behrend.d_value_pos

added theorem behrend.div_lt_floor

added theorem behrend.exists_large_sphere

added theorem behrend.exists_large_sphere_aux

added theorem behrend.exp_four_lt

added theorem behrend.exp_neg_two_mul_le

added theorem behrend.four_zero_nine_six_lt_exp_sixteen

added theorem behrend.le_N

added theorem behrend.le_sqrt_log

added theorem behrend.log_two_mul_two_le_sqrt_log_eight

added theorem behrend.lower_bound_le_one'

added theorem behrend.lower_bound_le_one

added theorem behrend.n_value_pos

added theorem behrend.roth_lower_bound

added theorem behrend.roth_lower_bound_explicit

added theorem behrend.three_le_n_value

added theorem behrend.two_div_one_sub_two_div_e_le_eight

added theorem behrend.two_le_n_value