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

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.