Prove the Brahmagupta-Fibonacci identity \[ (a^2 + b^2)(c^2 + d^2) = (ac - bd)^2 + (ad + bc)^2 \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := sorry
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
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
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
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
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
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
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
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
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