def a : ℕ → ℤ

Equations

• a t = Nat.strongRec (fun (n : ℕ) (a : (m : ℕ) → m < n → ℤ) => match n, a with | 0, a => 0 | 1, a => 1 | n.succ.succ, a => -∑ d ∈ (n + 1).divisors.attach, a ↑d ⋯) t

theorem a_simp : (a 0 = 0 ∧ a 1 = 1) ∧ ∀ (n : ℕ), a (n + 2) = -∑ d ∈ (n + 1).divisors, a d

theorem a_odd_le_double_pred (k : ℕ) (hk : Odd k) (H : ∀ m < 2 * k - 1, (Odd m → _root_.a m ≥ 0) ∧ (Even m → _root_.a m ≤ 0)) : a k ≤ a (2 * k - 1)

theorem a_odd_add_double_le_zero (k : ℕ) (hk : Odd k) (H : ∀ m < 2 * k, (Odd m → _root_.a m ≥ 0) ∧ (Even m → _root_.a m ≤ 0)) : a k + a (2 * k) ≤ 0

def oddPart (n : ℕ) : ℕ

Equations

• oddPart n = n / 2 ^ n.factorization 2

theorem oddPart_spec (n : ℕ) (h : n ≠ 0) : Odd (oddPart n) ∧ oddPart n * 2 ^ n.factorization 2 = n

theorem sum_geometric_progression_le_zero (t : ℕ) (ht : Odd t) (k : ℕ) (htk : t ∣ k) (H : ∀ m < 2 * k + 1, (Odd m → _root_.a m ≥ 0) ∧ (Even m → _root_.a m ≤ 0)) : ∑ d ∈ (2 * k).divisors with oddPart d = t, a d ≤ 0

theorem signs (n : ℕ) : (Odd n → _root_.a n ≥ 0) ∧ (Even n → _root_.a n ≤ 0)