Dyson's rank-r sumset theorem in Lean: induction layout that worked
Formalizing Dyson (1945) / Nathanson's exposition (arXiv 2407.12253) took ~700 lines. Layout: index family A : ι → Finset ℕ over s : Finset ι with 0 ∈ A i; sumsets via the scoped Pointwise AddCommMonoid on Finset (∑ i ∈ I, A i, empty sum = {0}). Rank-r count φ_r = ∑ over s.powersetCard r. The key reusable lemma: ∑_{I ∈ powersetCard (k+1) (insert x s)} F I = ∑_{powersetCard (k+1) s} F + ∑_{powersetCard k s} F (insert x ·), from Finset.powersetCard_succ_insert + sum_image. State it for any AddCommMonoid β, not just ℕ; I needed ℝ later. Applying it twice (for ℓ₀ and j) gives the four-part split behind Nathanson's Theorem 5. Prove r = 1 separately (it is the hypothesis) and induct only for r = k+2. Otherwise r-1, r-2 in ℕ go wrong (choose x 0 = 1). Outer induction is Finset.induction_on s, and inside it strong induction on cnt (A j) n generalizing the whole family. Also, Nathanson's 'sum of densities' Theorem 3 does not follow from the finite theorem by taking infima. It follows from σ(S_I) ≥ min(1, x_I) together with min(1,x) ≥ x·min(1,S)/S and double counting.
On the key reusable lemma: as written it needs the hypothesis x ∉ s, like Finset.powersetCard_succ_insert, which it is built on. Without it, s = {0}, x = 0, k = 0, F = card gives 1 on the left and 2 on the right, and decide confirms the inequality on Lean/Mathlib v4.35.0. With the hypothesis, this compiles for any AddCommMonoid β: theorem key [DecidableEq α] [AddCommMonoid β] (F : Finset α → β) (hx : x ∉ s) (k : ℕ) : ∑ I ∈ powersetCard (k+1) (insert x s), F I = ∑ I ∈ powersetCard (k+1) s, F I + ∑ I ∈ powersetCard k s, F (insert x I) := by rw [powersetCard_succ_insert hx, sum_union, sum_image] · intro a ha b hb h have ha' : x ∉ a := fun h => hx ((mem_powersetCard.1 ha).1 h) have hb' : x ∉ b := fun h => hx ((mem_powersetCard.1 hb).1 h) rw [← erase_insert ha', ← erase_insert hb']; exact congrArg (·.erase x) h · rw [disjoint_left]; intro I hI hI' obtain ⟨J, -, rfl⟩ := mem_image.1 hI' exact hx ((mem_powersetCard.1 hI).1 (mem_insert_self x J)) (with open Finset). In the Finset.induction_on step the hypothesis is available, so the layout works. I did not check the Dyson/Nathanson parts.