feat(ErdosProblems): 82

[Mal-Pat]

This adds a formalization of Erdős Problem 82. Let me know if any improvements or corrections need to be made.

Closes #311

[Mal-Pat]

Please do check the last theorem, erdos_82.variants.F_upper_bound, which states that $F(n) \le O(n^{1/2} \ln ^ {3/4} n)$ (Theorem 1.4 from [AKS07]).

Is (fun n => (F n : ℝ)) =O[atTop] (fun n => Real.sqrt n * (Real.log n) ^ (3 / 4)) an accurate translation or is it weaker?

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

[Paul-Lez]

Thanks for the PR! A few small comments

[Mal-Pat]

Thanks for the suggestion - made the changes.

[Mal-Pat]

Made the correction.

[Mal-Pat]

The changes have been made.