Large energy implies many popular pairs
ProvedFinset.popular_pairs_card_lower_boundadditive-combinatoricsadditive-energybalog-szemeredi-gowerspopular-sums
Let be an additive commutative group and finite sets with nonempty and . Suppose
where is the additive energy and counts representations . If satisfies , then the popular pairs are numerous:
The proof splits the energy sum into popular and unpopular fibres and uses the total-mass identity . This lemma quantifies the first half of the energy-to-graph conversion: truncating the convolution at level retains a constant fraction of all pairs, so that together with the Markov upper bound on the number of popular sums it produces the dense popular-sum graph.
Preamble
import Mathlib open scoped Pointwise
Formal statement
theorem Finset.popular_pairs_card_lower_bound {G : Type*} [AddCommGroup G] [DecidableEq G]
{η : ℝ} (_hη : 0 < η)
{X Y : Finset G} (hXY : X.card = Y.card) (hX : X.Nonempty)
(hE : η * (X.card : ℝ) ^ 3 ≤ (Finset.addEnergy X Y : ℝ))
(θ : ℕ) (hθ : 2 * (θ : ℝ) ≤ η * X.card) :
η / 2 * (X.card : ℝ) * Y.card ≤
(((X ×ˢ Y).filter
(fun p ↦ θ ≤ X.addConvolution Y (p.1 + p.2))).card : ℝ) := by sorry
Source
Popular/unpopular fibre split inside the proof of Tao-Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Lemma 2.30 (p. 80). Not separately stated in the cited work. Formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/Combinatorics/Additive/BalogSzemerediGowers.lean#L121-L213
Human review
Confirmed by the mission captain (proposal self-audit).