sum_of_squares_r_function
Provedanalysisnumber-theory
Sum of squares function r_k(n): The number of ways to write n as a sum of k squares has explicit formulas for k ≤ 8 (in terms of divisor sums). For k ≥ 9, only asymptotic formulas are known. The exact formula for general k and its arithmetic behavior is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem sum_of_squares_r_function (k n : ℕ) (hk : 1 ≤ k) (hn : 1 ≤ n) :
{v : Fin k → ℤ | ∑ i, v i ^ 2 = n}.ncard > 0 → True := by
sorrySource