Lemma 2.8 — |A_1 ∩ ⋯ ∩ A_p| ≥ Σ|A_i| − (p − 1)|A_1 ∪ ⋯ ∪ A_p|

Proved

WangKangXue.SpectralTuran.lemma_2_8

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $p \ge 1$ and let $A_1, \dots, A_p$ be finite sets. Then

|A_1 \cap \dots \cap A_p| \ \ge\ \sum_{i=1}^p |A_i| - (p-1)\,\Big|\bigcup_{i=1}^p A_i\Big| .

This elementary counting inequality is how the paper finds many common neighbours of a set of high-degree vertices inside one part, the step behind Lemmas 3.4–3.8.

Formalization Note The inequality is stated over $\mathbb Z$ . The hypothesis $p \ge 1$ is implicit on the page (at $p = 0$ the empty intersection is not a finite set).

Preamble

import Mathlib

Formal statement

namespace WangKangXue.SpectralTuran

open Classical

/-- **Lemma 2.8** (Wang–Kang–Xue, arXiv:2203.10831v1, p. 3; from Cioabă et al.). For finite sets
`A_1, …, A_p` (`p ≥ 1`),
`|A_1 ∩ ⋯ ∩ A_p| ≥ ∑_i |A_i| − (p − 1) |A_1 ∪ ⋯ ∪ A_p|`. -/
theorem lemma_2_8 {α : Type*} [DecidableEq α] (p : ℕ) (hp : 1 ≤ p) (A : Fin p → Finset α) :
    ((Finset.univ.inf' ⟨⟨0, hp⟩, Finset.mem_univ _⟩ A).card : ℤ) ≥
      ∑ i, ((A i).card : ℤ) - ((p : ℤ) - 1) * ((Finset.univ.biUnion A).card : ℤ) := by sorry

end WangKangXue.SpectralTuran

Source

Wang, Kang, Xue, On a conjecture of spectral extremal problems, arXiv:2203.10831v1, p. 3, Lemma 2.8 (from Cioabă, Feng, Tait, Zhang)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph