Skip to content

Erdős problem 82

Start work

F(n)/log⁡n→∞asn→∞F(n) / \log n \to \infty as n \to \infty

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

82.lean

Retained formal statement2 of 2

F(n)≤O(n1/2ln⁡3/4n)F(n) \le O(n^{1/2} \ln ^ {3/4} n)

Theorem 1.4 from [AKS07]

[AKS07] Alon, N. and Krivelevich, M. and Sudakov, B., Large nearly regular induced subgraphs. arXiv:0710.2106 (2007).

FormalConjectures/ErdosProblems/82.leanErdos82.erdos_82.variants.F_upper_bound1 lineExact file
(fun n => ↑(Erdos82.F n)) =O[Filter.atTop] fun n => √↑n * Real.log ↑n ^ (3 / 4)
SolvedStatement only, no proof