The Littlewood-Offord problem

theorem Finset.exists_littlewood_offord_partition {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι} {f : ι → E} {r : ℝ} [DecidableEq ι] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) : ∃ (P : Finpartition s.powerset), P.parts.card = s.card.choose (s.card / 2) ∧ (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun (u v : Finset ι) => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)

theorem Finset.card_le_of_forall_dist_sum_le {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝒜 : Finset (Finset ι)} {s : Finset ι} {f : ι → E} {r : ℝ} (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆ s) (hf : ∀ i ∈ s, r ≤ ‖f i‖) (h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r) : 𝒜.card ≤ s.card.choose (s.card / 2)

Kleitman's lemma