Documentation

FormalConjectures.Wikipedia.GaussCircleProblem

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. $$

source
@[reducible, inline]
noncomputable abbrev GaussCircleProblem.N (r : ℝ) :
ℕ

Let $N(r)$ be the number of points $(m, n)$ within a circle of radius $r$, where $m$ and $n$ are both integers.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev GaussCircleProblem.E (r : ℝ) :
    ℝ

    Let $E(r)$ be the error term between the number of integral points inside the circle and the area of the circle; that is $N(r) = \pi r^2 + E(r)$.

    Equations
    Instances For
      source
      theorem GaussCircleProblem.error_le :
      ∀ᶠ (r : ℝ) in Filter.atTop, |E r| ≤ 2 * √2 * Real.pi * r

      Gauss proved that $$ |E(r)|\leq 2\sqrt{2}\pi r, $$ for sufficiently large $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

      source
      theorem GaussCircleProblem.error_not_isLittleO :
      ¬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) $$

      source
      theorem GaussCircleProblem.error_isBigO :
      ∃ (o : ℝ → ℝ) (_ : Filter.Tendsto o Filter.atTop (nhds 0)), E ≪ 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

      source
      theorem GaussCircleProblem.exact_form_floor (r : ℝ) (hr : 0 ≤ r) :
      ↑(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). $$