Skip to main content

Nicomachus’s theorem

Induction

Prove the Nicomachus's theorem which states that the sum of the cubes of the first \(n\) natural numbers is equal to the square of the sum of the first \(n\) natural numbers; that is, for any natural number n we have \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic

open Nat

variable ( n : ℕ)

def sum : ℕ → ℕ
  | 0      => 0
  | succ n => sum n + (n+1)

def sumCubes : ℕ → ℕ
  | 0   => 0
  | n+1 => sumCubes n + (n+1)^3

example :
  sumCubes n = (sum n)^2 :=
by sorry

Read more…

If uₙ tends to a y vₙ tends to b, then uₙvₙ tends to ab

Limits

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

It is defined that the sequence \(u\) tends to \(c\) by:

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

Prove that if \(u_n\) tends to \(a\) and \(v_n\) tends to \(b\), then \(u_nv_n\) tends to \(ab\).

To do this, complete the following Lean4 theory:

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

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

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

example
  (hu : TendsTo u a)
  (hv : TendsTo v b)
  : TendsTo (fun n ↦ u n * v n) (a * b) :=
by sorry

Read more…

If the limit of the sequence u(n) is a and c ∈ ℝ, then the limit of u(n)c is ac

Limits

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…

If u(n) tends to a, then 7u(n) tends to 7a

Limits

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…

Pigeonhole principle

Finite sets

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…

If f ∘ f is bijective, then f is bijective

Functions

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…