FormalConjectures/ErdosProblems/162.lean

GitHub source file

8 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos162.colourEdgeCount The number of edges of $K_n$ inside H that get colour b under the colouring c line 36 source

   Source documentation

   The number of edges of $K_n$ inside H that get colour b under the colouring c.

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

   Statement uses: Nat, Sym2, Fin, Bool, Finset

   Proof uses: Finset.card, Finset.filter, And, Not, Sym2.IsDiag, Eq, Finset.sym2

   5 instances, coercions and auxiliary constants left out.

   def colourEdgeCount {n : ℕ} (c : Sym2 (Fin n) → Bool) (H : Finset (Fin n)) (b : Bool) : ℕ :=
   …

   Mentions: c

2. def Erdos162.IsBalancedAbove Every set H of at least k vertices contains more than $\alpha\binom{|H|}{2}$ edges of each colour under c line 41 source

   Source documentation

   Every set H of at least k vertices contains more than $\alpha\binom{|H|}{2}$ edges of each colour under c.

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

   Statement uses: Nat, Real, Sym2, Fin, Bool

   Proof uses: Finset, LE.le, Finset.card, LT.lt, HMul.hMul, Nat.choose, OfNat.ofNat, Erdos162.colourEdgeCount

   7 instances, coercions and auxiliary constants left out.

   def IsBalancedAbove (n : ℕ) (α : ℝ) (c : Sym2 (Fin n) → Bool) (k : ℕ) : Prop :=
   …

   Mentions: c

3. def Erdos162.F $F(n, \alpha)$: the smallest k such that some 2-colouring of $K_n$ satisfies IsBalancedAbove n α c k line 50 source

   Source documentation

   $F(n, \alpha)$: the smallest k such that some 2-colouring of $K_n$ satisfies IsBalancedAbove n α c k.

   The source says "largest k". Read literally, every k > n works vacuously, so no largest k exists. The smallest k is the reading consistent with the stated $\Theta(\log n)$ growth.

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

   Statement uses: Nat, Real

   Proof uses: InfSet.sInf, Set.ofPred, Exists, Sym2, Fin, Bool, Erdos162.IsBalancedAbove

   1 instances, coercions and auxiliary constants left out.

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

4. theorem Erdos162.erdos_162 Let $\alpha > 0$ and $n \geq 1$ sorry line 65 source

   Source documentation

   Let $\alpha > 0$ and $n \geq 1$. Let $F(n,\alpha)$ be the largest $k$ such that there exists some 2-colouring of the edges of $K_n$ in which any induced subgraph $H$ on at least $k$ vertices contains more than $\alpha\binom{|H|}{2}$ many edges of each colour.

   Prove that for every fixed $0 \leq \alpha \leq 1/2$, as $n \to \infty$, $F(n,\alpha) \sim c_\alpha \log n$ for some constant $c_\alpha$.

   We require $\alpha < 1/2$: at $\alpha = 1/2$ no colouring works for any k ≤ n (see erdos_162.variants.half).

   depends on sorry what this means

   Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, Nat, Exists, Asymptotics.IsEquivalent, Filter.atTop, Erdos162.F, HMul.hMul, Real.log

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

   46 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_162 (α : ℝ) (h0 : 0 ≤ α) (h1 : α < 1 / 2) :
       ∃ c : ℝ, (fun n : ℕ ↦ (F n α : ℝ)) ~[atTop] (fun n : ℕ ↦ c * Real.log n) := by
   …

   Mentions: c, Erdos162.F

5. theorem Erdos162.erdos_162.variants.bounds It is easy to show with the probabilistic method that there exist $c_1(\alpha), c_2(\alpha)$ such that $c_1(\alpha)\log n < F(n,\alpha) < c_2(\alpha)\log n$ sorry line 74 source

   Source documentation

   It is easy to show with the probabilistic method that there exist $c_1(\alpha), c_2(\alpha)$ such that $c_1(\alpha)\log n < F(n,\alpha) < c_2(\alpha)\log n$.

   depends on sorry what this means

   Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, Nat, Exists, And, Filter.Eventually, HMul.hMul, Real.log, Erdos162.F, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, 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_162.variants.bounds (α : ℝ) (h0 : 0 ≤ α) (h1 : α < 1 / 2) :
       ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ c₁ < c₂ ∧ ∀ᶠ n : ℕ in atTop,
         c₁ * Real.log n < F n α ∧ (F n α : ℝ) < c₂ * Real.log n := by
   …

   Mentions: Erdos162.F

6. theorem Erdos162.erdos_162.variants.half At $\alpha = 1/2$ the two colour counts in $H$ add up to $\binom{|H|}{2}$, so both cannot exceed half of it sorry line 84 source

   Source documentation

   At $\alpha = 1/2$ the two colour counts in $H$ add up to $\binom{|H|}{2}$, so both cannot exceed half of it. Hence $F(n, 1/2) = n + 1$, and the claim fails at $\alpha = 1/2$.

   depends on sorry what this means

   Statement uses: Nat, Eq, Erdos162.F, HDiv.hDiv, Real, OfNat.ofNat, HAdd.hAdd

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

   24 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_162.variants.half (n : ℕ) : F n (1 / 2) = n + 1 := by
   …

   Mentions: Erdos162.F

7. theorem Erdos162.isBalancedAbove_succ k = n + 1 always works, since no vertex set has more than n elements line 89 source

   Source documentation

   k = n + 1 always works, since no vertex set has more than n elements.

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

   Statement uses: Nat, Real, Sym2, Fin, Bool, Erdos162.IsBalancedAbove, HAdd.hAdd, OfNat.ofNat

   Proof uses: Finset, LE.le, Finset.card, Fintype.card, Finset.card_le_univ, Decidable.byContradiction, LT.lt, HMul.hMul, Nat.choose, Erdos162.colourEdgeCount, Not, Eq.mp, congrArg, Fintype.card_fin

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

   theorem isBalancedAbove_succ (n : ℕ) (α : ℝ) (c : Sym2 (Fin n) → Bool) :
       IsBalancedAbove n α c (n + 1) := by
   …

   Mentions: c, Erdos162.IsBalancedAbove

8. theorem Erdos162.F_le_succ $F(n, \alpha)$ is at most n + 1 line 98 source

   Source documentation

   $F(n, \alpha)$ is at most n + 1.

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

   Statement uses: Nat, Real, LE.le, Erdos162.F, HAdd.hAdd, OfNat.ofNat

   Proof uses: Nat.sInf_le, Set.ofPred, Exists, Sym2, Fin, Bool, Erdos162.IsBalancedAbove, Exists.intro, Bool.true, Erdos162.isBalancedAbove_succ

   7 instances, coercions and auxiliary constants left out.

   theorem F_le_succ (n : ℕ) (α : ℝ) : F n α ≤ n + 1 :=
   …

   Mentions: Erdos162.F