Proofs of ∑k<n. 2ᵏ = 2ⁿ-1
Prove that \[ 1 + 2 + 2^2 + 2^3 + ... + 2^{n-1} = 2^n - 1 \]
To do this, complete the following Lean4 theory:
import Mathlib.Tactic open Finset Nat variable (n : ℕ) example : ∑ k in range n, 2^k = 2^n - 1 := by sorry
Proofs of "∑i<n. i = n(n-1)/2"
Gauss's formula for the sum of the first natural numbers is \[ 0 + 1 + 2 + ... + (n-1) = \dfrac{n(n-1)}{2} \] that is, \[ \sum_{i < n} i = \dfrac{n(n-1)}{2} \]
In a previous exercise, this formula was proven by induction. Another way to prove it, without using induction, is the following: The sum can be written in two ways \begin{align} S &= &0 &+ &1 &+ &2 &+ ... &+ &(n-3) &+ &(n-2) &+ &(n-1) \newline S &= &(n-1) &+ &(n-2) &+ &(n-3) &+ ... &+ &2 &+ &1 &+ &0 \end{align} By adding, we observe that each pair of numbers in the same column sums to (n-1), and since there are n columns in total, it follows that \[ 2S = n(n-1) \] which proves the formula.
Prove Gauss's formula by following the above procedure.
To do this, complete the following Lean4 theory:
import Mathlib.Algebra.BigOperators.Intervals import Mathlib.Tactic open Finset Nat variable (n i : ℕ) example : ∑ i ∈ range n, i = n * (n - 1) / 2 := by sorry
Proofs of "If p > -1, then (1+p)ⁿ ≥ 1+np"
Let \(p ∈ ℝ\) and \(n ∈ ℕ\). Prove that if \(p > -1\), then \[ (1 + p)^n ≥ 1 + np \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic open Nat variable (p : ℝ) variable (n : ℕ) example (h : p > -1) : (1 + p)^n ≥ 1 + n*p := by sorry
Proofs of 0³+1³+2³+3³+···+n³ = (n(n+1)/2)²
Prove that the sum of the first cubes \[ 0^3 + 1^3 + 2^3 + 3^3 + ··· + n^3 \] is \[ \dfrac{n(n+1)}{2}^2 \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Nat.Defs import Mathlib.Tactic open Nat variable (n : ℕ) def sumCubes : ℕ → ℕ | 0 => 0 | n+1 => sumCubes n + (n+1)^3 example : 4 * sumCubes n = (n*(n+1))^2 := by sorry
Proofs of a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)
Prove that if \(q ≠ 1\), then the sum of the terms of the geometric progression \[ a + aq + aq^2 + ··· + aq^n \] is \[ \dfrac{a(1 - q^{n+1})}{1 - q} \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Nat.Defs import Mathlib.Tactic open Nat variable (n : ℕ) variable (a q : ℝ) def sumGP : ℝ → ℝ → ℕ → ℝ | a, _, 0 => a | a, q, n + 1 => sumGP a q n + (a * q^(n + 1)) example (h : q ≠ 1) : sumGP a q n = a * (1 - q^(n + 1)) / (1 - q) := by sorry
Proofs of a+(a+d)+(a+2d)+···+(a+nd)=(n+1)(2a+nd)/2
Prove that the sum of the terms of the arithmetic progression \[ a + (a + d) + (a + 2d) + ··· + (a + nd) \] is \[ \dfrac{(n + 1)(2a + nd)}{2} \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Nat.Defs import Mathlib.Tactic open Nat variable (n : ℕ) variable (a d : ℝ) def sumAP : ℝ → ℝ → ℕ → ℝ | a, _, 0 => a | a, d, n + 1 => sumAP a d n + (a + (n + 1) * d) example : 2 * sumAP a d n = (n + 1) * (2 * a + n * d) := by sorry
Proofs of "0+1+2+3+···+n=n(n + 1)/2"
Prove that the sum of the natural numbers \[ 0 + 1 + 2 + 3 + ··· + n \] is \[\dfrac{n(n + 1)}{2}\]
To do this, complete the following Lean4 theory:
import Init.Data.Nat.Basic import Mathlib.Tactic open Nat variable (n : Nat) set_option pp.fieldNotation false def sum : Nat → Nat | 0 => 0 | succ n => sum n + (n+1) example : 2 * sum n = n * (n + 1) := by sorry
If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)
In Lean4, we can define that \(a\) is the limit of the sequence \(u\) by:
def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε
and that \(f\) is continuous at \(a\) by:
def continuous_at (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε
To prove that if the function \(f\) is continuous at the point \(a\), and the sequence \(u(n)\) converges to \(a\), then the sequence \(f(u(n))\) converges to \(f(a)\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} variable {a : ℝ} variable {u : ℕ → ℝ} def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε def continuous_at (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε example (hf : continuous_at f a) (hu : is_limit u a) : is_limit (f ∘ u) (f a) := by sorry
If x is the limit of u and y is an upper bound of u, then x ≤ y
In Lean4, we can define that \(a\) is the limit of the sequence \(u\) by:
def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε
and that \(a\) is an upper bound of \(u\) by:
def is_upper_bound (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a
Prove that if \(x\) is the limit of the sequence \(u\) and \(y\) is an upper bound of \(u\), then \(x ≤ y\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u : ℕ → ℝ) variable (x y : ℝ) def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε def is_upper_bound (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a example (hx : is_limit u x) (hy : is_upper_bound u y) : x ≤ y := by sorry
If (∀ ε > 0, y ≤ x + ε), then y ≤ x
Let \(x, y ∈ ℝ\). Prove that \[ (∀ ε > 0, y ≤ x + ε) → y ≤ x \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x y : ℝ} example : (∀ ε > 0, y ≤ x + ε) → y ≤ x := by sorry