Gauss circle problem

Reference: Wikipedia

Gauss Circle Problem

Consider a circle in $\mathbb{R}^2$ with center at the origin and radius $r\geq 0$. Gauss's circle problem asks how many points there are inside this circle of the form $(m, n)$ where $m$ and $n$ are both integers. Equivalently, how many pairs of integers $m$ and $n$ are there such that $$ m^2 + n^2 \leq r^2. $$

theorem GaussCircleProblem.error_le (r : ℝ) (hr : 0 ≤ r) : |GaussCircleProblem.E✝ r| ≤ 2 * √2 * Real.pi * r

Gauss proved that $$ |E(r)|\leq 2\sqrt{2}\pi r. $$

[Ha59] Hardy, G. H. (1959). Ramanujan: Twelve Lectures on Subjects Suggested by His Life and Work(3rd ed.). New York: Chelsea Publishing Company. p. 67

theorem GaussCircleProblem.error_not_isLittleO (r : ℝ) (hr : 0 ≤ r) : ¬GaussCircleProblem.E✝ =o[Filter.atTop] fun (r : ℝ) => √r * √√(Real.log r)

Hardy and Laundau independently found a lower bound by showing that $$ |E(r)| \neq o\left(r^{1/2}(\log r)^{1/4}\right) $$

theorem GaussCircleProblem.error_isBigO : ∃ (o : ℝ → ℝ) (_ : Filter.Tendsto o Filter.atTop (nhds 0)), GaussCircleProblem.E✝ =O[Filter.atTop] fun (r : ℝ) => r ^ (1 / 2 + o r)

It is conjectured that the correct bound is $$ |E(r)| = O\left(r^{1/2 + o(1)})\right) $$

[Ha59] Hardy, G. H. (1959). Ramanujan: Twelve Lectures on Subjects Suggested by His Life and Work(3rd ed.). New York: Chelsea Publishing Company. p. 67

See also https://arxiv.org/abs/2305.03549

theorem GaussCircleProblem.exact_form_floor (r : ℝ) (hr : 0 ≤ r) : ↑(GaussCircleProblem.N✝ r) = 1 + 4 * ∑' (i : ℝ), (⌊r ^ 2 / (4 * i + 1)⌋ - ⌊r ^ 2 / (4 * i + 3)⌋)

The value of $N(r)$ can be expressed as $$ N(r) = 1 + 4\sum_{i=0}^{\infty}\left(\left\lfloor\frac{r^2}{4i+1}\right\rfloor - \left\lfloor\frac{r^2}{4i + 3}\right\rfloor\right). $$