Rationals.Limits

Andrew Sneap, November 2021

In this file I define the limit for sequences of rational numbers,
and prove that 2/3^n converges by first proving the sandwich theorem,
and that 1/(n+1) converges to 0.

\begin{code}

{-# OPTIONS --safe --without-K --lossy-unification #-}

open import MLTT.Spartan renaming (_+_ to _∔_)

open import Notation.Order
open import UF.Base
open import UF.FunExt
open import UF.Subsingletons
open import UF.PropTrunc
open import Rationals.Type
open import Rationals.Addition
open import Rationals.Abs
open import Rationals.Multiplication
open import Rationals.Negation
open import Rationals.Order
open import Rationals.Positive hiding (_+_ ; _*_)
open import Rationals.FractionsOrder
open import Rationals.FractionsOperations renaming (_*_ to _𝔽*_) hiding (abs ; -_ ; _+_)
open import Naturals.Addition renaming (_+_ to _ℕ+_)
open import Naturals.Division
open import Naturals.Multiplication renaming (_*_ to _ℕ*_)
open import Naturals.Order
open import Naturals.Properties
open import Integers.Type hiding (abs)
open import Integers.Addition renaming (_+_ to _ℤ+_) hiding (_-_)
open import Integers.Order
open import Integers.Multiplication renaming (_*_ to _ℤ*_)

module Rationals.Limits
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (pt : propositional-truncations-exist)
 where

open import MetricSpaces.Rationals fe pe pt

_⟶_ : (f : ℕ → ℚ) → (L : ℚ) → 𝓤₀ ̇
f ⟶ L = (ε₊@(ε , _) : ℚ₊) → Σ N ꞉ ℕ , ((n : ℕ) → N ≤ n → abs (f n - L) < ε)

sandwich-theorem : (L : ℚ)
                 → (f g h : ℕ → ℚ)
                 → Σ N ꞉ ℕ , ((n : ℕ) → N ≤ n → f n ≤ g n ≤ h n)
                 → f ⟶ L
                 → h ⟶ L
                 → g ⟶ L
sandwich-theorem L f g h (N , α) f⟶L h⟶L = γ
 where
  γ : g ⟶ L
  γ ε₊@(ε , _) = γ' (f⟶L ε₊) (h⟶L ε₊)
   where
    γ' : Σ N₁ ꞉ ℕ , ((n : ℕ) → N₁ ≤ n → abs (f n - L) < ε)
       → Σ N₂ ꞉ ℕ , ((n : ℕ) → N₂ ≤ n → abs (h n - L) < ε)
       → Σ M ꞉ ℕ , ((n : ℕ) → M ≤ n → abs (g n - L) < ε)
    γ' (N₁ , β) (N₂ , δ) = M , γ''
     where
      M : ℕ
      M = max (max N₁ N₂) N

      I : N ≤ M
      I = max-≤-upper-bound' N (max N₁ N₂)

      II : N₁ ≤ max N₁ N₂
      II = max-≤-upper-bound N₁ N₂

      III : N₂ ≤ max N₁ N₂
      III = max-≤-upper-bound' N₂ N₁

      IV : max N₁ N₂ ≤ M
      IV = max-≤-upper-bound (max N₁ N₂) N

      V : N₁ ≤ M
      V = ≤-trans N₁ (max N₁ N₂) M II IV

      VI : N₂ ≤ M
      VI = ≤-trans N₂ (max N₁ N₂) M III IV

      γ'' : (n : ℕ) → max (max N₁ N₂) N ≤ n → abs (g n - L) < ε
      γ'' n l = ℚ<-to-abs (g n - L) ε (γ₁ , γ₂)
       where
        VII : - ε < f n - L < ε
        VII = ℚ-abs-<-unpack (f n - L) ε (β n (≤-trans N₁ M n V l))

        VIII : - ε < h n - L < ε
        VIII = ℚ-abs-<-unpack (h n - L) ε (δ n (≤-trans N₂ M n VI l))

        l₁ : f n ≤ g n ≤ h n
        l₁ = α n (≤-trans N (max (max N₁ N₂) N) n I l)

        IX : f n - L ≤ g n - L
        IX = ℚ≤-addition-preserves-order (f n) (g n) (- L) (pr₁ l₁)

        X : g n - L ≤ h n - L
        X = ℚ≤-addition-preserves-order (g n) (h n) (- L) (pr₂ l₁)

        γ₁ : - ε < g n - L
        γ₁ = ℚ<-≤-trans (- ε) (f n - L) (g n - L) (pr₁ VII) IX

        γ₂ : g n - L < ε
        γ₂ = ℚ≤-<-trans (g n - L) (h n - L) ε X (pr₂ VIII)

0f : ℕ → ℚ
0f _ = 0ℚ

0f-converges : 0f ⟶ 0ℚ
0f-converges ε₊@(ε , 0<ε) = 0 , (λ n _ → 0<ε)

constant-sequence : (q : ℚ) → (n : ℕ) → ℚ
constant-sequence q n = q

constant-sequence-converges : (q : ℚ) → (constant-sequence q) ⟶ q
constant-sequence-converges q (ε , 0<ε) = 0 , γ
 where
  γ : (n : ℕ) → 0 ≤ n → abs (constant-sequence q n - q) < ε
  γ n _ = transport (_< ε) I 0<ε
   where
    I : 0ℚ ＝ abs (constant-sequence q n - q)
    I = ℚ-zero-dist q ⁻¹

⟨2/3⟩^_ : ℕ → ℚ
⟨2/3⟩^ 0         = toℚ (pos 1 , 0)
⟨2/3⟩^ (succ n)  = rec 2/3 (_* 2/3) n

⟨2/3⟩-to-mult : (n : ℕ) → ⟨2/3⟩^ (succ n) ＝ (⟨2/3⟩^ n) * 2/3
⟨2/3⟩-to-mult 0 = refl
⟨2/3⟩-to-mult (succ n) = refl

⟨2/3⟩^n-positive : (n : ℕ) → 0ℚ < (⟨2/3⟩^ n)
⟨2/3⟩^n-positive 0 = 0 , refl
⟨2/3⟩^n-positive (succ n) = transport (0ℚ <_) γ II
 where
  I : 0ℚ < (⟨2/3⟩^ n)
  I = ⟨2/3⟩^n-positive n

  II : 0ℚ < (⟨2/3⟩^ n) * 2/3
  II = ℚ<-pos-multiplication-preserves-order (⟨2/3⟩^ n) 2/3 I (1 , refl)

  γ : (⟨2/3⟩^ n) * 2/3 ＝ (⟨2/3⟩^ (succ n))
  γ = ⟨2/3⟩-to-mult n ⁻¹

⟨2/3⟩-all-positive : (n : ℕ) → 0ℚ ≤ (⟨2/3⟩^ n)
⟨2/3⟩-all-positive n = γ
 where
  I : 0ℚ < (⟨2/3⟩^ n)
  I = ⟨2/3⟩^n-positive n

  γ : 0ℚ ≤ (⟨2/3⟩^ n)
  γ = ℚ<-coarser-than-≤ 0ℚ (⟨2/3⟩^ n) I

⟨1/n⟩ : ℕ → ℚ
⟨1/n⟩ n = toℚ (pos 1 , n)

⟨1/sn⟩ : ℕ → ℚ
⟨1/sn⟩ 0 = 1ℚ
⟨1/sn⟩ (succ n) = ⟨1/n⟩ n

⟨1/n⟩-1 : ⟨1/n⟩ 0 ＝ 1ℚ
⟨1/n⟩-1 = refl

⟨1/n⟩-1/2 : ⟨1/n⟩ 1 ＝ 1/2
⟨1/n⟩-1/2 = refl

⟨1/2⟩^_ : ℕ → ℚ
⟨1/2⟩^ 0         = toℚ (pos 1 , 0)
⟨1/2⟩^ (succ n)  = rec (1/2) (_* 1/2) n

⟨1/sn⟩-converges-lemma : (a n x q r : ℕ)
                       → succ a ＝ q ℕ* succ x ℕ+ r
                       → r < succ x
                       → succ q ≤ succ n
                       → pos (succ a) < pos (succ n) ℤ* pos (succ x)
⟨1/sn⟩-converges-lemma a n x q r e l₁ l₂ = γ
 where
  x' = succ x
  q' = succ q
  a' = succ a
  n' = succ n

  I : pos r < pos x'
  I = ℕ-order-respects-ℤ-order r x' l₁

  II : pos (q ℕ* x') ℤ+ pos r < pos (q ℕ* x') ℤ+ pos x'
  II = ℤ<-adding-left (pos r) (pos x') (pos (q ℕ* x')) I

  III : pos (q ℕ* x') ℤ+ pos r ＝ pos a'
  III = pos (q ℕ* x') ℤ+ pos r ＝⟨ distributivity-pos-addition (q ℕ* x') r ⟩
        pos (q ℕ* x' ℕ+ r)     ＝⟨ ap pos (e ⁻¹)                           ⟩
        pos a'               ∎

  IV : pos (q ℕ* x') ℤ+ pos x' ＝ pos q' ℤ* pos x'
  IV = pos (q ℕ* x') ℤ+ pos x' ＝⟨ i   ⟩
       pos x' ℤ+ pos (q ℕ* x') ＝⟨ ii  ⟩
       pos x' ℤ+ pos (x' ℕ* q) ＝⟨ iii ⟩
       pos x' ℤ* pos q'        ＝⟨ iv  ⟩
       pos q' ℤ* pos x'        ∎
   where
    i   = ℤ+-comm (pos (q ℕ* x')) (pos x')
    ii  = ap (λ ■ → pos x' ℤ+ (pos ■)) (mult-commutativity q x')
    iii = ap (pos x' ℤ+_) (pos-multiplication-equiv-to-ℕ x' q ⁻¹)
    iv  = ℤ*-comm (pos x') (pos q')

  V : pos a' < pos q' ℤ* pos x'
  V = transport₂ _<_ III IV II

  VI : pos q' ≤ pos n'
  VI = ℕ≤-to-ℤ≤ q' n' l₂

  VII : pos q' ℤ* pos x' ≤ pos n' ℤ* pos x'
  VII = positive-multiplication-preserves-order' (pos q') (pos n') (pos x') ⋆ VI

  γ : pos a' < pos n' ℤ* pos x'
  γ = ℤ<-≤-trans (pos a') (pos q' ℤ* pos x') (pos n' ℤ* pos x') V VII

⟨1/sn⟩-converges : ⟨1/sn⟩ ⟶ 0ℚ
⟨1/sn⟩-converges (ε@((pos 0 , a) , p) , 0<ε) = 𝟘-elim γ
 where
  I : ε ＝ 0ℚ
  I = numerator-zero-is-zero ((pos 0 , a) , p) refl

  II : 0ℚ < 0ℚ
  II = transport (0ℚ <_) I 0<ε

  γ : 𝟘
  γ = ℚ<-irrefl 0ℚ II
⟨1/sn⟩-converges ε₊@(((negsucc x , a) , p) , 0<ε) = 𝟘-elim γ
 where
  γ : 𝟘
  γ = negative-not-greater-than-zero x a 0<ε
⟨1/sn⟩-converges ε₊@(((pos (succ x) , a) , p) , 0<ε) = γ (division (succ a) x)
 where
  γ : Σ q ꞉ ℕ , Σ r ꞉ ℕ , (succ a ＝ q ℕ* succ x ℕ+ r) × (r < succ x)
    → Σ N ꞉ ℕ , ((n : ℕ) → N ≤ n → abs (⟨1/sn⟩ n - 0ℚ) < ε₊)
  γ (q , r , e , l₁) = succ q , γ'
   where
    γ' : (n : ℕ)
       → succ q < succ n
       → abs (⟨1/sn⟩ n - 0ℚ) <ℚ ((pos (succ x) , a) , p)
    γ' 0 l₂ = 𝟘-elim l₂
    γ' (succ n) l₂ = γ''
     where
      I : pos 0 ＝ pos 0 ℤ* pos (succ n)
      I = ℤ-zero-left-base (pos (succ n)) ⁻¹

      II : pos 0 ℤ* pos (succ n) < pos 1
      II = transport (_< pos 1) I (0 , refl)

      III : 0ℚ < toℚ (pos 1 , n)
      III = toℚ-< (pos 0 , 0) (pos 1 , n) II

      IV : toℚ (pos 1 , n) ＝ abs (⟨1/n⟩ n + 0ℚ)
      IV = toℚ (pos 1 , n)       ＝⟨ i  ⟩
           abs (toℚ (pos 1 , n)) ＝⟨ ii ⟩
           abs (⟨1/n⟩ n + 0ℚ)    ∎
       where
        i  = abs-of-pos-is-pos' (toℚ (pos 1 , n)) III ⁻¹
        ii = ap abs (ℚ-zero-right-neutral (⟨1/n⟩ n)) ⁻¹

      V : toℚ (pos (succ x) , a) ＝ ((pos (succ x) , a) , p)
      V = toℚ-to𝔽 ((pos (succ x) , a) , p) ⁻¹

      VI : pos (succ a) < pos (succ n) ℤ* pos (succ x)
      VI = ⟨1/sn⟩-converges-lemma a n x q r e l₁ l₂

      VII : (pos 1 , n) 𝔽< (pos (succ x) , a)
      VII = positive-order-flip a n x 0 VI

      VIII : toℚ (pos 1 , n) < toℚ (pos (succ x) , a)
      VIII = toℚ-< (pos 1 , n) (pos (succ x) , a) VII

      γ'' : abs (⟨1/n⟩ n - 0ℚ) <ℚ ((pos (succ x) , a) , p)
      γ'' = transport₂ _<_ IV V VIII

⟨1/sn⟩-bounds-⟨2/3⟩-lemma : (n : ℕ)
                          → (⟨1/sn⟩ (succ (succ n))) * 2/3
                          ≤ ⟨1/sn⟩ (succ (succ (succ n)))
⟨1/sn⟩-bounds-⟨2/3⟩-lemma n = γ
 where
  n+2 = succ (succ n)
  n+3 = succ (n+2)

  1' = pos 1
  2' = pos 2
  3' = pos 3
  6' = pos 6
  n' = pos n

  I : 2' ℤ* n' ℤ+ 6' ＝ 2' ℤ* pos (n ℕ+ 3)
  I = 2' ℤ* n' ℤ+ 6'      ＝⟨ distributivity-mult-over-ℤ' n' 3' 2' ⁻¹       ⟩
      2' ℤ* (n' ℤ+ 3')    ＝⟨ ap (2' ℤ*_) (distributivity-pos-addition n 3) ⟩
      2' ℤ* pos (n ℕ+ 3)  ∎

  II : 3' ℤ* n' ℤ+ 6' ＝ 1' ℤ* pos (succ (pred (n+2 ℕ* 3)))
  II = 3' ℤ* n' ℤ+ 6'                     ＝⟨ i   ⟩
       pos (3 ℕ* n) ℤ+ 6'                 ＝⟨ ii  ⟩
       pos (3 ℕ* n ℕ+ 6)                  ＝⟨ iii ⟩
       pos (3 ℕ* n+2)                     ＝⟨ iv  ⟩
       pos (n+2 ℕ* 3)                     ＝⟨ v   ⟩
       pos (succ (pred (n+2 ℕ* 3)))       ＝⟨ vi  ⟩
       1' ℤ* pos (succ (pred (n+2 ℕ* 3))) ∎
   where
    i   = ap (_ℤ+ 6') (pos-multiplication-equiv-to-ℕ 3 n)
    ii  = distributivity-pos-addition (3 ℕ* n) 6
    iii = ap pos (distributivity-mult-over-addition 3 n 2 ⁻¹)
    iv  = ap pos (mult-commutativity 3 n+2)
    v   = ap pos (succ-pred-multiplication (succ n) 2)
    vi  = ℤ-mult-left-id _ ⁻¹

  III : pos 0 ≤ n'
  III = ℤ-zero-least-pos n

  IV : 2' ℤ* n' ≤ 3' ℤ* n'
  IV = ℤ*-multiplication-order 2' 3' n' III (1 , refl)

  V : 2' ℤ* n' ℤ+ 6' ≤ 3' ℤ* n' ℤ+ 6'
  V = ℤ≤-adding' (2' ℤ* n') (3' ℤ* n') 6' IV

  VI : 2' ℤ* pos n+3 ≤ 1' ℤ* pos (succ (pred (n+2 ℕ* 3)))
  VI = transport₂ _≤_ I II V

  VII : toℚ ((1' , succ n) 𝔽* (2' , 2)) ≤ toℚ (1' , n+2)
  VII = toℚ-≤ ((1' , succ n) 𝔽* (2' , 2)) (1' , n+2) VI

  VIII : toℚ ((1' , succ n) 𝔽* (2' , 2)) ＝ toℚ (1' , succ n) * 2/3
  VIII = toℚ-* (1' , succ n) (2' , 2)

  γ : (⟨1/sn⟩ n+2) * 2/3 ≤ ⟨1/sn⟩ n+3
  γ = transport (_≤ ⟨1/sn⟩ n+3) VIII VII

⟨1/sn⟩-bounds-⟨2/3⟩ : (n : ℕ) → (⟨2/3⟩^ n) ≤ ⟨1/sn⟩ n
⟨1/sn⟩-bounds-⟨2/3⟩ = ℕ-induction base step
 where
  base : 1ℚ ≤ 1ℚ
  base = 0 , refl

  step : (n : ℕ) → (⟨2/3⟩^ n) ≤ (⟨1/sn⟩ n) → (⟨2/3⟩^ succ n) ≤ ⟨1/sn⟩ (succ n)
  step 0 IH = 1 , refl
  step 1 IH = 1 , refl
  step (succ (succ n)) IH = γ
   where
    S₁⦅n+2⦆ = ⟨2/3⟩^ (succ (succ n))
    S₁⦅n+3⦆ = ⟨2/3⟩^ (succ (succ (succ n)))
    S₂⦅n+2⦆ = ⟨1/sn⟩ (succ (succ n))
    S₂⦅n+3⦆ = ⟨1/sn⟩ (succ (succ (succ n)))

    I : S₁⦅n+2⦆ * 2/3 ≤ S₂⦅n+2⦆ * 2/3
    I = ℚ≤-pos-multiplication-preserves-order' S₁⦅n+2⦆ S₂⦅n+2⦆  2/3 IH (2 , refl)

    II : S₂⦅n+2⦆ * 2/3 ≤ S₂⦅n+3⦆
    II = ⟨1/sn⟩-bounds-⟨2/3⟩-lemma n

    γ : S₁⦅n+3⦆ ≤ S₂⦅n+3⦆
    γ = ℚ≤-trans (S₁⦅n+2⦆ * 2/3) (S₂⦅n+2⦆ * 2/3) S₂⦅n+3⦆ I II

⟨2/3⟩^n-squeezed : Σ N ꞉ ℕ  , ((n : ℕ) → (N ≤ n) → (0f n ≤ ⟨2/3⟩^ n ≤ ⟨1/sn⟩ n))
⟨2/3⟩^n-squeezed = 1 , γ
 where
  γ : (n : ℕ) → 1 ≤ n → (0f n ≤ ⟨2/3⟩^ n ≤ ⟨1/sn⟩ n)
  γ n l = γ₁ , γ₂
   where
    γ₁ : 0ℚ ≤ (⟨2/3⟩^ n)
    γ₁ = ⟨2/3⟩-all-positive n

    γ₂ : (⟨2/3⟩^ n) ≤ (⟨1/sn⟩ n)
    γ₂ = ⟨1/sn⟩-bounds-⟨2/3⟩ n

⟨2/3⟩^n-converges : ⟨2/3⟩^_ ⟶ 0ℚ
⟨2/3⟩^n-converges =
 sandwich-theorem
  0ℚ 0f ⟨2/3⟩^_ ⟨1/sn⟩
   ⟨2/3⟩^n-squeezed
   0f-converges
   ⟨1/sn⟩-converges

⟨2/3⟩^n<ε : (ε : ℚ₊) → Σ n ꞉ ℕ , (⟨2/3⟩^ n) < ε
⟨2/3⟩^n<ε ε = γ (⟨2/3⟩^n-converges ε)
 where
  γ : Σ N ꞉ ℕ , ((n : ℕ) → N ≤ n → abs ((⟨2/3⟩^ n) - 0ℚ) < ε)
    → Σ n ꞉ ℕ , (⟨2/3⟩^ n) < ε
  γ (N , f) = N , γ'
   where
    I : abs ((⟨2/3⟩^ N) - 0ℚ) < ε
    I = f N (≤-refl N)

    II : 0ℚ < (⟨2/3⟩^ N)
    II = ⟨2/3⟩^n-positive N

    III : abs ((⟨2/3⟩^ N) - 0ℚ) ＝ ⟨2/3⟩^ N
    III = abs ((⟨2/3⟩^ N) + 0ℚ) ＝⟨ ap abs (ℚ-zero-right-neutral (⟨2/3⟩^ N)) ⟩
          abs (⟨2/3⟩^ N)        ＝⟨ abs-of-pos-is-pos' (⟨2/3⟩^ N) II         ⟩
          (⟨2/3⟩^ N)            ∎

    γ' : (⟨2/3⟩^ N) < ε
    γ' = transport (_< ε) III I

⟨2/3⟩^n<ε-consequence : (ε (p , _) : ℚ₊) → Σ n ꞉ ℕ , (⟨2/3⟩^ n) * p < ε
⟨2/3⟩^n<ε-consequence (ε , 0<ε) (p , 0<p) = γ (⟨2/3⟩^n<ε (ε * p' , 0<εp'))
 where
  p-not-zero : ¬ (p ＝ 0ℚ)
  p-not-zero = ℚ<-positive-not-zero p 0<p

  p' : ℚ
  p' = ℚ*-inv p p-not-zero

  0<p' : 0ℚ < p'
  0<p' = ℚ-inv-preserves-pos p 0<p p-not-zero

  0<εp' : 0ℚ < ε * p'
  0<εp' = ℚ<-pos-multiplication-preserves-order ε p' 0<ε 0<p'

  γ : Σ n ꞉ ℕ , (⟨2/3⟩^ n) < ε * p'
    → Σ n ꞉ ℕ , (⟨2/3⟩^ n) * p < ε
  γ (n , l) = n , γ'
   where
    I : (⟨2/3⟩^ n) * p < ε * p' * p
    I = ℚ<-pos-multiplication-preserves-order' (⟨2/3⟩^ n) (ε * p') p l 0<p

    II : ε * p' * p ＝ ε
    II = ε * p' * p   ＝⟨ ℚ*-assoc ε p' p                             ⟩
         ε * (p' * p) ＝⟨ ap (ε *_) (ℚ*-comm p' p)                    ⟩
         ε * (p * p') ＝⟨ ap (ε *_) (ℚ*-inverse-product p p-not-zero) ⟩
         ε * 1ℚ       ＝⟨ ℚ-mult-right-id ε                           ⟩
         ε            ∎

    γ' : (⟨2/3⟩^ n) * p < ε
    γ' = transport ((⟨2/3⟩^ n) * p <_) II I

\end{code}