FormalConjectures/ErdosProblems/161.lean

GitHub source file

2 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos161.erdos_161.parts.i Let $\alpha\in[0,1/2)$ and $n,t\geq 1$ sorry line 48 source

   Source documentation

   Let $\alpha\in[0,1/2)$ and $n,t\geq 1$. Let $F^{(t)}(n,\alpha)$ be the smallest $m$ such that we can $2$-colour the edges of the complete $t$-uniform hypergraph on $n$ vertices such that if $X\subseteq [n]$ with $\lvert X\rvert \geq m$ then there are at least $\alpha \binom{\lvert X\rvert}{t}$ many $t$-subsets of $X$ of each colour. For fixed $n,t$ as we change $\alpha$ from $0$ to $1/2$ does $F^{(t)}(n,\alpha)$ increase continuously or are there jumps? Only one jump?

   Here growth is compared up to constant factors as $n\to\infty$. At $\alpha=0$, each color must occur, following the source's Ramsey convention.

   depends on sorry what this means

   Statement uses: Nat, Set, Prod, Real, sorryAx, Bool.false, LE.le, OfNat.ofNat, Eq, Set.ofPred, And, Membership.mem, Set.Ico, HDiv.hDiv, Prod.fst, Prod.snd, Asymptotics.IsTheta, Filter.atTop, Hypergraph.balancedColoringThreshold

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

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_161.parts.i :
       let E : ℕ → Set (ℝ × ℝ) := answer(sorry)
   …

2. theorem Erdos161.erdos_161.parts.ii For fixed $t\geq 3$, do all positive densities below $1/2$ give the same asymptotic order? sorry line 60 source

   Source documentation

   For fixed $t\geq 3$, do all positive densities below $1/2$ give the same asymptotic order?

   depends on sorry what this means

   Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Real, LT.lt, HDiv.hDiv, Asymptotics.IsTheta, Filter.atTop, Hypergraph.balancedColoringThreshold

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

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_161.parts.ii :
       answer(sorry) ↔ ∀ t : ℕ, 3 ≤ t → ∀ α β : ℝ,
       0 < α → α < 1 / 2 → 0 < β → β < 1 / 2 →
       (fun n ↦ (Hypergraph.balancedColoringThreshold n t α : ℝ)) =Θ[atTop]
         (fun n ↦ (Hypergraph.balancedColoringThreshold n t β : ℝ)) := by
   …

   Mentions: Hypergraph.balancedColoringThreshold