Ir al contenido principal

Proofs of "∑i<n. i = n(n-1)/2"

Summation

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

Leer más…

Proofs of "If p > -1, then (1+p)ⁿ ≥ 1+np"

Induction

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

Leer más…

Proofs of 0³+1³+2³+3³+···+n³ = (n(n+1)/2)²

Induction

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

Leer más…

Proofs of a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)

Induction

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

Leer más…

Proofs of a+(a+d)+(a+2d)+···+(a+nd)=(n+1)(2a+nd)/2

Induction

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

Leer más…

Proofs of "0+1+2+3+···+n=n(n + 1)/2"

Induction

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

Leer más…

If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)

Limits

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

Leer más…

If x is the limit of u and y is an upper bound of u, then x ≤ y

Limits

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

Leer más…

If (∀ ε > 0, y ≤ x + ε), then y ≤ x

Real numbers

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

Leer más…

If x is the supremum of set A, then ((∀ y)[y < x → (∃ a ∈ A)[y < a]]

Real numbers

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

Leer más…