Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 18:30 44999a92

View on Github →

feat(combinatorics/additive/behrend): Behrend's construction (#14070) Construct large Salem-Spencer sets in ℕ using Behrend's construction. The idea is to turn the Euclidean sphere into a discrete set of points in Euclidean space which we then squash onto ℕ.

Estimated changes

added theorem zero_pow_le_one
added def behrend.box
added theorem behrend.box_zero
added theorem behrend.card_box
added def behrend.map
added theorem behrend.map_eq_iff
added theorem behrend.map_inj_on
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 def behrend.sphere
added theorem behrend.sum_eq
added theorem behrend.sum_lt