theoremfactorial_sum (n : ℕ) : (∑ k ∈ Finset.range (n + 1), k * Nat.factorial k) + 1 = Nat.factorial (n + 1) := by induction n with | zero => simp | succ m ih => rw [Finset.sum_range_succ] ...
theoremtwo_mul_le_sq_add_sq : ∀ a b : ℝ, 2 * (a * b) ≤ a ^ 2 + b ^ 2 := by intro a b; have h := sq_nonneg_real (a - b); rw [expand_sub_sq] at h; lina...
theoremerdos_discrepancy : ∀ (s : ℕ→ ({-1, 1} : Set ℤ)), ∀ C : ℝ, ∃ d n : ℕ, 0 < d ∧ 0 < n ∧ C < |∑ k ∈ Finset.range n, (s (d * (k + 1)) : ℝ)| := sorry
theoremlagrange_four_squares (n : ℕ) : ∃ a b c d : ℕ, n = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 := by obtain ⟨a, b, c, d, h⟩ := Nat.sum_four_squares n use a, b, c, d rw [h]