FormalConjectures/ErdosProblems/1105.lean

GitHub source file

2 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos1105.erdos_1105.parts.i The anti-Ramsey number sorry line 52 source

   Source documentation

   The anti-Ramsey number $\mathrm{AR}(n,G)$ is the maximum possible number of colours in which the edges of $K_n$ can be coloured without creating a rainbow copy of $G$ (i.e. one in which all edges have different colours).

   Let $C_k$ be the cycle on $k$ vertices. Is it true that $\mathrm{AR}(n,C_k)=\left(\frac{k-2}{2}+\frac{1}{k-1}\right)n+O(1)$?

   Montellano-Ballesteros and Neumann-Lara [MoNe05] gave an exact formula for $\mathrm{AR}(n,C_k)$, which implies in particular that $\mathrm{AR}(n,C_k)=\left(\frac{k-2}{2}+\frac{1}{k-1}\right)n+O(1).$

   depends on sorry what this means

   Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Asymptotics.IsBigO, Real, Filter.atTop, HSub.hSub, SimpleGraph.antiRamseyNum, Fin, SimpleGraph.cycleGraph, HMul.hMul, HAdd.hAdd, HDiv.hDiv

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

   42 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1105.parts.i : answer(True) ↔
       ∀ k, 3 ≤ k →
       ((fun n => (antiRamseyNum (cycleGraph k) n : ℝ) - ((k - 2 : ℝ) / 2 + 1 / (k - 1)) * n)
         =O[atTop] (fun _ => (1 : ℝ))) := by
   …

2. theorem Erdos1105.erdos_1105.parts.ii Let $P_k$ be the path on $k$ vertices and $\ell=\lfloor\frac{k-1}{2}\rfloor$ sorry line 68 source

   Source documentation

   Let $P_k$ be the path on $k$ vertices and $\ell=\lfloor\frac{k-1}{2}\rfloor$. If $n\geq k\geq 5$ then is $\mathrm{AR}(n,P_k)$ equal to $\max\left(\binom{k-2}{2}+1, \binom{\ell-1}{2}+(\ell-1)(n-\ell+1)+\epsilon\right)$where $\epsilon=1$ if $k$ is odd and $\epsilon=2$ otherwise?

   A proof of the formula for $\mathrm{AR}(n,P_k)$ for all $n\geq k\geq 5$ has been announced by Yuan [Yu21].

   depends on sorry what this means

   Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, HDiv.hDiv, HSub.hSub, ite, Odd, Eq, SimpleGraph.antiRamseyNum, Fin, SimpleGraph.pathGraph, Max.max, HAdd.hAdd, Nat.choose, HMul.hMul

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

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1105.parts.ii : answer(True) ↔
       ∀ (k n : ℕ), 5 ≤ k → k ≤ n →
       let ℓ := (k - 1) / 2
   …