FormalConjectures/ErdosProblems/643.lean

GitHub source file

2 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos643.erdos_643.parts.i Documented declaration: i sorry line 47 source

   Source documentation

   Let $f(n;t)$ be minimal such that if a $t$-uniform hypergraph on $n$ vertices contains at least $f(n;t)$ edges then there must be four edges $A,B,C,D$ such that $$A\cup B= C\cup D$$ and $$A\cap B=C\cap D=\emptyset.$$ Estimate $f(n;t)$ - in particular, is it true that for $t\geq 3$ $$f(n;t)=(1+o(1))\binom{n}{t-1}?$$

   depends on sorry what this means

   Statement uses: Nat, Real, sorryAx, Bool.false, LE.le, OfNat.ofNat, Asymptotics.IsEquivalent, Filter.atTop, HAdd.hAdd, Hypergraph.extremalNumber, Finset, Fin, Not, Finset.HasRepeatedDisjointUnion

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_643.parts.i :
       let f : ℕ → ℕ → ℝ := answer(sorry)
   …

2. theorem Erdos643.erdos_643.parts.ii Is it true that $f(n;t)=(1+o(1))\binom{n}{t-1}$ for $t\geq 3$? sorry line 58 source

   Source documentation

   Is it true that $f(n;t)=(1+o(1))\binom{n}{t-1}$ for $t\geq 3$?

   depends on sorry what this means

   Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Asymptotics.IsEquivalent, Real, Filter.atTop, HAdd.hAdd, Hypergraph.extremalNumber, Finset, Fin, Not, Finset.HasRepeatedDisjointUnion, Nat.choose, HSub.hSub

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

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_643.parts.ii :
       answer(sorry) ↔ ∀ t : ℕ, 3 ≤ t →
       (fun n ↦ ((Hypergraph.extremalNumber n t
         (fun H ↦ ¬ H.HasRepeatedDisjointUnion) + 1 : ℕ) : ℝ)) ~[atTop]
           (fun n ↦ (n.choose (t - 1) : ℝ)) := by
   …

   Mentions: Hypergraph.extremalNumber