Prove2Me

Lemma 3: shifting to an initial family keeps the size and does not increase ν\nu

Proved
FranklKupavskii2022.EMC.initial_family_exists

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

extremal-set-theoryp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1shifting

Let m,k≥0m,k\ge0. For every family F~⊆([m]k)\tilde{\mathcal F}\subseteq\binom{[m]}{k} there is an initial family F⊆([m]k)\mathcal F\subseteq\binom{[m]}{k} with

∣F∣=∣F~∣andν(F)≤ν(F~).|\mathcal F|=|\tilde{\mathcal F}|\quad\text{and}\quad \nu(\mathcal F)\le\nu(\tilde{\mathcal F}).

Consequently, in the Erdős matching problem one may restrict attention to initial (shifted) families. The lemma is due to Frankl (1987) and is quoted in the paper without proof.

Preamble
import Mathlib
import Definitions.Def_FranklKupavskii2022_EMC_matchingNumber
import Definitions.Def_FranklKupavskii2022_EMC_IsInitial
Formal statement
namespace FranklKupavskii2022.EMC

/-- Lemma 3 (Frankl–Kupavskii, arXiv:1806.08855v3, p. 3, citing Frankl 1987 [13]): for every
family `F̃ ⊂ \binom{[m]}{k}` there is an initial family `F ⊂ \binom{[m]}{k}` with `|F| = |F̃|` and
`ν(F) ≤ ν(F̃)`.

**Formalization Note.** `[m] = Finset.Icc 1 m`; "initial" is `IsInitial m k`, whose downward
closure ranges over `k`-subsets of `[m]`. -/
theorem initial_family_exists (m k : ℕ) (Ft : Finset (Finset ℕ))
    (hFt : Ft ⊆ (Finset.Icc 1 m).powersetCard k) :
    ∃ F : Finset (Finset ℕ), F ⊆ (Finset.Icc 1 m).powersetCard k ∧ IsInitial m k F ∧
      F.card = Ft.card ∧ matchingNumber F ≤ matchingNumber Ft := by sorry

end FranklKupavskii2022.EMC
Source
Frankl–Kupavskii, The Erdős Matching Conjecture and concentration inequalities, arXiv:1806.08855v3, Lemma 3, p. 3 (citing [13] Frankl 1987)
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph