Erdős Problem 624

Reference: erdosproblems.com/624

def Erdos624.ExistsEventuallySurjective (n m : ℕ) : Prop

The condition that an integer m ensures the existence of a function f covering Fin n for all large enough subsets Y. The property is invariant under bijection, so we use a representative Fin n for a finite set of size n.

Equations

• Erdos624.ExistsEventuallySurjective n m = ∃ (f : Finset (Fin n) → Fin n), ∀ (Y : Finset (Fin n)), Y.card ≥ m → Finset.image f Y.powerset = Finset.univ

noncomputable def Erdos624.H (n : ℕ) : ℕ

Let $H(n)$ be the minimum integer $m$ such that there is a function $f: \mathcal{P}(X) \to X$ where $X$ is a finite set of size $n$, such that for every subset $Y \subseteq X$ with $|Y| \ge m$, the set $\{f(A) : A \subseteq Y\}$ covers $X$.

Equations

• Erdos624.H n = if 0 < n then sInf {m : ℕ | Erdos624.ExistsEventuallySurjective n m} else 0

theorem Erdos624.erdos_624 : Filter.Tendsto (fun (n : ℕ) => ↑(H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop

Let $X$ be a finite set of size $n$ and $H(n)$ be such that there is a function $f:\{A : A\subseteq X\}\to X$ so that for every $Y\subseteq X$ with $\lvert Y\rvert \geq H(n)$ we have $\left\{ f(A) : A\subseteq Y\right\}=X$. Prove that $H(n)-\log_2 n \to \infty$.