Commit 2023-06-06 11:47 6dea3c8f

View on Github →

feat: port Combinatorics.Additive.Behrend (#4730)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Additive/Behrend.lean

added theorem Behrend.addSalemSpencer_image_sphere

added theorem Behrend.bound

added theorem Behrend.bound_aux'

added theorem Behrend.bound_aux

added def Behrend.box

added theorem Behrend.box_zero

added theorem Behrend.card_box

added theorem Behrend.card_sphere_le_rothNumberNat

added theorem Behrend.ceil_lt_mul

added theorem Behrend.dValue_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 def Behrend.map

added theorem Behrend.map_eq_iff

added theorem Behrend.map_injOn

added theorem Behrend.map_le_of_mem_box

added theorem Behrend.map_mod

added theorem Behrend.map_monotone

added theorem Behrend.map_succ'

added theorem Behrend.map_succ

added theorem Behrend.map_zero

added theorem Behrend.mem_box

added theorem Behrend.nValue_pos

added theorem Behrend.norm_of_mem_sphere

added theorem Behrend.roth_lower_bound

added theorem Behrend.roth_lower_bound_explicit

added def Behrend.sphere

added theorem Behrend.sphere_subset_box

added theorem Behrend.sphere_subset_preimage_metric_sphere

added theorem Behrend.sphere_zero_right

added theorem Behrend.sphere_zero_subset

added theorem Behrend.sum_eq

added theorem Behrend.sum_lt

added theorem Behrend.sum_sq_le_of_mem_box

added theorem Behrend.three_le_nValue

added theorem Behrend.two_div_one_sub_two_div_e_le_eight

added theorem Behrend.two_le_nValue