In Lean, a sequence \(u_₀, u_₁, u_₂, ... \) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is \(u_n\).

It is defined that \(a\) is the limit of the sequence \(u\), by

   def limite : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

Prove that if the limit of \(u_n\) is \(a\), then the limit of \(u_nc\) is \(ac\).

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (u : ℕ → ℝ)
variable (a c : ℝ)

def TendsTo : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : TendsTo u a)
  : TendsTo (fun n ↦ (u n) * c) (a * c) :=
by sorry

Read more…

In Lean, a sequence \(u_0, u_1, u_2, ...\) can be represented by a function \(u : ℕ → ℝ\) such that \(u(n)\) is the term \(u_n\).

We define that \(u\) tends to \(a\) by

   def tendsTo : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

Prove that if \(u_n\) tends to \(a\), then \(7u\_n\) tends to \(7a\).

To do this, complete the following Lean4 theory:

import Mathlib.Tactic

variable {u : ℕ → ℝ}
variable {a : ℝ}

def tendsTo : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : tendsTo u a)
  : tendsTo (fun n ↦ 7 * u n) (7 * a) :=
by sorry

Read more…

Prove the pigeonhole principle; that is, if \(S\) is a finite set and \(T\) and \(U\) are subsets of \(S\) such that the number of elements of \(S\) is less than the sum of the number of elements of \(T\) and \(U\), then the intersection of \(T\) and \(U\) is non-empty.

To do this, complete the following Lean4 theory:

import Mathlib.Data.Finset.Card

open Finset

variable [DecidableEq α]
variable {s t u : Finset α}

set_option pp.fieldNotation false

example
  (hts : t ⊆ s)
  (hus : u ⊆ s)
  (hstu : card s < card t + card u)
  : Finset.Nonempty (t ∩ u) :=
by sorry

Read more…

Prove that if \(f ∘ f\) is bijective, then \(f\) is bijective.

To do this, complete the following Lean4 theory:

import Mathlib.Tactic
open Function

variable {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (f : X → X)
  (h : Bijective (f ∘ f))
  : Bijective f :=
by sorry

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…