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
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
In Lean4, one can define that \(x\) is an upper bound of \(A\) by
def is_upper_bound (A : Set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x
and \(x\) is supremum of \(A\) by
def is_supremum (A : Set ℝ) (x : ℝ) := is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y
Prove that if \(x\) is the supremum of \(A\), then \[ (∀ y)[y < x → (∃ a ∈ A)[y < a]] \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic variable {A : Set ℝ} variable {x : ℝ} def is_upper_bound (A : Set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x def is_supremum (A : Set ℝ) (x : ℝ) := is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y example (hx : is_supremum A x) : ∀ y, y < x → ∃ a ∈ A, y < a := by sorry
In Lean4, the Fibonacci function can be defined as
def fibonacci : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fibonacci n + fibonacci (n+1)
Another more efficient definition is
def fib (n : Nat) : Nat := (loop n).1 where loop : Nat → Nat × Nat | 0 => (0, 1) | n + 1 => let p := loop n (p.2, p.1 + p.2)
Prove that both definitions are equivalent; that is,
fibonacci = fib
To do this, complete the following Lean4 theory:
open Nat set_option pp.fieldNotation false def fibonacci : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fibonacci n + fibonacci (n+1) def fib (n : Nat) : Nat := (loop n).1 where loop : Nat → Nat × Nat | 0 => (0, 1) | n + 1 => let p := loop n (p.2, p.1 + p.2) example : fibonacci = fib := by sorry
The tree corresponding to
3 / \ 2 4 / \ 1 5
can be represented by the term
Node 3 (Node 2 (Leaf 1) (Leaf 5)) (Leaf 4)
using the datatype defined by
inductive Tree' (α : Type) : Type | Leaf : α → Tree' α | Node : α → Tree' α → Tree' α → Tree' α
The mirror image of the previous tree is
3 / \ 4 2 / \ 5 1
and the list obtained by flattening it (traversing it in infix order) is
[4, 3, 5, 2, 1]
The definition of the function that calculates the mirror image is
def mirror : Tree' α → Tree' α | Leaf x => Leaf x | Node x l r => Node x (mirror r) (mirror l)
and the one that flattens the tree is
def flatten : Tree' α → List α | Leaf x => [x] | Node x l r => (flatten l) ++ [x] ++ (flatten r)
Prove that
flatten (mirror a) = reverse (flatten a)
To do this, complete the following Lean4 theory:
import Mathlib.Tactic open List variable {α : Type} set_option pp.fieldNotation false inductive Tree' (α : Type) : Type | Leaf : α → Tree' α | Node : α → Tree' α → Tree' α → Tree' α namespace Tree' variable (a l r : Tree' α) variable (x : α) def mirror : Tree' α → Tree' α | Leaf x => Leaf x | Node x l r => Node x (mirror r) (mirror l) def flatten : Tree' α → List α | Leaf x => [x] | Node x l r => (flatten l) ++ [x] ++ (flatten r) example : flatten (mirror a) = reverse (flatten a) := by sorry