FormalConjectures/Wikipedia/GaussCircleProblem.lean

GitHub source file

6 declarations, 4 contain sorry, 0 declared as axioms

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

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Real, Nat

   Proof uses: Set.ncard, Prod, Int, Set.ofPred, GaussCircleProblem.N.match_1, Membership.mem, WithLp, OfNat.ofNat, ENNReal, Fin, Set, EuclideanSpace, Metric.closedBall, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty

   23 instances, coercions and auxiliary constants left out.

   noncomputable abbrev N (r : ℝ) : ℕ :=
   …

2. abbrev GaussCircleProblem.E 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)$ line 56 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Real

   Proof uses: HSub.hSub, GaussCircleProblem.N, HMul.hMul, Real.pi, HPow.hPow, Nat, OfNat.ofNat

   11 instances, coercions and auxiliary constants left out.

   noncomputable abbrev E (r : ℝ) : ℝ := N r - π * r ^ 2
   …

   Mentions: GaussCircleProblem.N

3. theorem GaussCircleProblem.error_le Gauss proved that $$ |E(r)|\leq 2\sqrt{2}\pi r, $$ for sufficiently large $r$ sorry line 68 source

   Source documentation

   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

   depends on sorry what this means

   Statement uses: Filter.Eventually, Real, LE.le, abs, GaussCircleProblem.E, HMul.hMul, OfNat.ofNat, Nat, Real.sqrt, Real.pi, Filter.atTop

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

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem error_le : ∀ᶠ r in atTop, |E r| ≤ 2 * √2 * π * r := by
   …

   Mentions: GaussCircleProblem.E

4. theorem GaussCircleProblem.error_not_isLittleO Hardy and Laundau independently found a lower bound by showing that $$ |E(r)| \neq o\left(r^{1/2}(\log r)^{1/4}\right) $$ sorry line 78 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Not, Asymptotics.IsLittleO, Real, Filter.atTop, GaussCircleProblem.E, HMul.hMul, Real.sqrt, Real.log

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

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem error_not_isLittleO : ¬E =o[atTop] (fun r => √r * √√r.log) := by
   …

   Mentions: GaussCircleProblem.E

5. theorem GaussCircleProblem.error_isBigO It is conjectured that the correct bound is $$ |E(r)| = O\left(r^{1/2 + o(1)}\right) $$ [Ha59] Hardy, G sorry line 92 source

   Source documentation

   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

   depends on sorry what this means

   Statement uses: Exists, Real, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, Asymptotics.IsBigO, GaussCircleProblem.E, HPow.hPow, HAdd.hAdd, HDiv.hDiv, Nat

   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 error_isBigO : ∃ (o : ℝ → ℝ) (_ : Tendsto o atTop (𝓝 0)),
       E =O[atTop] fun r => r ^ (1/2 + o r) := by
   …

   Mentions: GaussCircleProblem.E

6. theorem GaussCircleProblem.exact_form_floor 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). $$ sorry line 104 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Real, LE.le, OfNat.ofNat, Eq, Int, GaussCircleProblem.N, HAdd.hAdd, HMul.hMul, tsum, Nat, HSub.hSub, Int.floor, HDiv.hDiv, HPow.hPow, SummationFilter.unconditional

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

   66 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem exact_form_floor (r : ℝ) (hr : 0 ≤ r) :
       N r = 1 + 4 * ∑' (i : ℕ), (⌊r ^ 2 / (4 * i + 1)⌋ - ⌊r ^ 2 / (4 * i + 3)⌋) := by
   …

   Mentions: GaussCircleProblem.N