Staver's identity

TheoremSplitting a power of minus one#✓fully proved

For natural numbers \(k \le n\), we have \((-1)^{n-k} \cdot (-1)^k = (-1)^n\) in \(\mathbb{Q}\).

theorem staver_sign_mul (n k : ℕ) (hk : k ≤ n) :
    (-1 : ℚ) ^ (n - k) * (-1 : ℚ) ^ k = (-1 : ℚ) ^ n
Used by 2
Used byReflecting a power of minus one, even case · Reflecting a power of minus one, odd case

TheoremSquares of powers of minus one#✓fully proved

For every natural number \(k\), we have \((-1)^k \cdot (-1)^k = 1\) in \(\mathbb{Q}\).

theorem staver_sign_sq (k : ℕ) : (-1 : ℚ) ^ k * (-1 : ℚ) ^ k = 1
Used by 2
Used byReflecting a power of minus one, even case · Reflecting a power of minus one, odd case

TheoremReflecting a power of minus one, odd case#✓fully proved

If \(n\) is an odd natural number and \(k \le n\) is a natural number, then \((-1)^{n-k} = -(-1)^k\) in \(\mathbb{Q}\).

theorem staver_sign_odd {n k : ℕ} (hodd : Odd n) (hk : k ≤ n) :
    (-1 : ℚ) ^ (n - k) = -(-1 : ℚ) ^ k
Uses 2 · Used by 1
Proof usesSplitting a power of minus one · Squares of powers of minus one
Used byStaver's identity for alternating reciprocal binomial sums

TheoremReflecting a power of minus one, even case#✓fully proved

If \(n\) is an even natural number and \(k \le n\) is a natural number, then \((-1)^{n-k} = (-1)^k\) in \(\mathbb{Q}\).

theorem staver_sign_even {n k : ℕ} (heven : Even n) (hk : k ≤ n) :
    (-1 : ℚ) ^ (n - k) = (-1 : ℚ) ^ k
Uses 2 · Used by 1
Proof usesSplitting a power of minus one · Squares of powers of minus one
Used byStaver's identity for alternating reciprocal binomial sums

TheoremReflection of the alternating reciprocal binomial sum#✓fully proved

For every natural number \(n\), \(\sum_{k=0}^{n} (-1)^{n-k} \binom{n}{k}^{-1} = \sum_{k=0}^{n} (-1)^{k} \binom{n}{k}^{-1}\) in \(\mathbb{Q}\).

theorem staver_reflect_zero (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
      (-1 : ℚ) ^ (n - k) * ((Nat.choose n k : ℚ))⁻¹) =
    ∑ k ∈ Finset.range (n + 1),
      (-1 : ℚ) ^ k * ((Nat.choose n k : ℚ))⁻¹
Used by 1
Used byStaver's identity for alternating reciprocal binomial sums

TheoremReflection of the weighted alternating reciprocal binomial sum#✓fully proved

For every natural number \(n\), \(\sum_{k=0}^{n} (-1)^{n-k} \, k \binom{n}{k}^{-1} = \sum_{k=0}^{n} (-1)^{k} (n-k) \binom{n}{k}^{-1}\) in \(\mathbb{Q}\).

theorem staver_reflect_one (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
      (-1 : ℚ) ^ (n - k) * (k : ℚ) * ((Nat.choose n k : ℚ))⁻¹) =
    ∑ k ∈ Finset.range (n + 1),
      (-1 : ℚ) ^ k * ((n - k : ℕ) : ℚ) * ((Nat.choose n k : ℚ))⁻¹
Used by 1
Used byStaver's identity for alternating reciprocal binomial sums

TheoremStaver's identity for alternating reciprocal binomial sums#✓fully proved

For a natural number \(n\), let \(S_0(n) = \sum_{k=0}^{n} (-1)^{n-k} \binom{n}{k}^{-1}\) and \(S_1(n) = \sum_{k=0}^{n} (-1)^{n-k} \, k \binom{n}{k}^{-1}\), computed in \(\mathbb{Q}\). If \(n\) is even, then \(S_1(n) = \frac{n}{2} S_0(n)\); if \(n\) is odd, then \(S_0(n) = 0\).

theorem staver_identity (n : ℕ) :
    (Even n →
      ∑ k ∈ Finset.range (n + 1), (-1 : ℚ) ^ (n - k) * (k : ℚ) * ((Nat.choose n k : ℚ))⁻¹ =
        (n : ℚ) / 2 * ∑ k ∈ Finset.range (n + 1), (-1 : ℚ) ^ (n - k) * ((Nat.choose n k : ℚ))⁻¹) ∧
    (Odd n →
      ∑ k ∈ Finset.range (n + 1), (-1 : ℚ) ^ (n - k) * ((Nat.choose n k : ℚ))⁻¹ = 0)
Sources
Uses 4
Proof usesReflection of the weighted alternating reciprocal binomial sum · Reflection of the alternating reciprocal binomial sum · Reflecting a power of minus one, even case · Reflecting a power of minus one, odd case

TheoremStaver's identity for reciprocal binomial sums#✓fully proved

For every natural number \(n\), the following identity between rational numbers holds:

\[\sum_{k=0}^{n} \binom{n}{k}^{-1} = \frac{n+1}{2^{n+1}} \sum_{k=1}^{n+1} \frac{2^k}{k}.\]

Both sides satisfy the recurrence \(F(n+1) = 1 + \frac{n+2}{2(n+1)} F(n)\) and both equal \(1\) at \(n = 0\), so the identity follows by induction on \(n\).

public theorem staver_reciprocal_binomial_sum (n : Nat) :
    (Finset.range (n + 1)).sum (fun k => ((Nat.choose n k : Rat))⁻¹) =
      ((n + 1 : Rat) / (2 : Rat) ^ (n + 1)) *
        (Finset.Icc 1 (n + 1)).sum (fun k => (2 : Rat) ^ k / (k : Rat))
Sources
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.