FormalConjectures/ErdosProblems/563.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

1. def Erdos563.HasBalancedSubsets Documented declaration: HasBalancedSubsets line 41 source

   Source documentation

   A 2-coloring of $K_n$ (represented by graph $G$ on $\mathrm{Fin}\; n$) is balanced on subsets of size at least $m$ with parameter $\alpha$ if every $X \subseteq [n]$ with $|X| \geq m$ contains more than $\alpha \binom{|X|}{2}$ edges of each color.

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

   Statement uses: Nat, Real, SimpleGraph, Fin

   Proof uses: Finset, LE.le, Finset.card, And, LT.lt, HMul.hMul, Nat.choose, OfNat.ofNat, Sym2, SimpleGraph.edgeFinset, SimpleGraph.induce, Subtype, Membership.mem, Set, Function.Embedding, Function.Embedding.subtype, Classical.propDecidable, SimpleGraph.Adj, HSub.hSub

   21 instances, coercions and auxiliary constants left out.

   def HasBalancedSubsets (n : ℕ) (m : ℕ) (α : ℝ) (G : SimpleGraph (Fin n)) : Prop :=
   …

2. def Erdos563.F Documented declaration: F line 52 source

   Source documentation

   $F(n,\alpha)$ is the smallest $m$ such that there exists a 2-coloring of the edges of $K_n$ so that every $X\subseteq [n]$ with $|X|\geq m$ contains more than $\alpha\binom{|X|}{2}$ edges of each color.

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

   Statement uses: Nat, Real

   Proof uses: InfSet.sInf, Set.ofPred, Exists, SimpleGraph, Fin, Erdos563.HasBalancedSubsets

   1 instances, coercions and auxiliary constants left out.

   noncomputable def F (n : ℕ) (α : ℝ) : ℕ :=
   …

3. theorem Erdos563.erdos_563 Documented declaration: erdos_563 sorry line 67 source

   Source documentation

   Let $F(n,\alpha)$ denote the smallest $m$ such that there exists a $2$-colouring of the edges of $K_n$ so that every $X\subseteq [n]$ with $\lvert X\rvert\geq m$ contains more than $\alpha \binom{\lvert X\rvert}{2}$ many edges of each colour.

   Prove that, for every $0\leq \alpha < 1/2$, $$F(n,\alpha)\sim c_\alpha\log n$$ for some constant $c_\alpha$ depending only on $\alpha$.

   This problem is #39 in Ramsey Theory in the graphs problem collection.

   depends on sorry what this means

   Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, Nat, Exists, And, Filter.Tendsto, Erdos563.F, Real.log, Filter.atTop, nhds

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

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_563 :
       ∀ (α : ℝ), 0 ≤ α → α < 1 / 2 →
         ∃ (c : ℝ), 0 < c ∧
           Tendsto (fun n : ℕ => (F n α : ℝ) / Real.log n) atTop (nhds c) := by
   …

   Mentions: c, Erdos563.F