FormalConjectures/ErdosProblems/624.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 624

Reference: erdosproblems.com/624

Imports (1)
  1. def Erdos624.ExistsEventuallySurjective The condition that an integer m ensures the existence of a function f covering Fin n for all large enough subsets Y line 38 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: Exists, Finset, Fin, GE.ge, Finset.card, Eq, Finset.image, Finset.powerset, Finset.univ

    3 instances, coercions and auxiliary constants left out.

    def ExistsEventuallySurjective (n m : ℕ) : Prop :=
…
  2. def Erdos624.H Documented declaration: H line 48 source

    Source documentation

    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$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: ite, LT.lt, OfNat.ofNat, InfSet.sInf, Set.ofPred, Erdos624.ExistsEventuallySurjective

    4 instances, coercions and auxiliary constants left out.

    noncomputable def H (n : ℕ) : ℕ :=
…
  3. theorem Erdos624.erdos_624 Documented declaration: erdos_624 sorry line 60 source

    Source documentation

    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$.

    depends on sorry what this means

    Statement uses: Filter.Tendsto, Nat, Real, HSub.hSub, Erdos624.H, Real.logb, OfNat.ofNat, Filter.atTop

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_624 :
    atTop.Tendsto (fun n : ℕ => H n - Real.logb 2 (n : ℝ)) atTop := by
…

    Mentions: Erdos624.H