Geometric sequences of real numbers

Content created by Louis Wasserman.

Created on 2025-11-10.
Last modified on 2025-11-10.

{-# OPTIONS --lossy-unification #-}

module real-numbers.geometric-sequences-real-numbers where
Imports 
open import commutative-algebra.geometric-sequences-commutative-rings

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import lists.sequences

open import metric-spaces.limits-of-sequences-metric-spaces
open import metric-spaces.uniformly-continuous-functions-metric-spaces

open import real-numbers.absolute-value-real-numbers
open import real-numbers.apartness-real-numbers
open import real-numbers.convergent-series-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.difference-real-numbers
open import real-numbers.isometry-difference-real-numbers
open import real-numbers.large-ring-of-real-numbers
open import real-numbers.limits-sequences-real-numbers
open import real-numbers.lipschitz-continuity-multiplication-real-numbers
open import real-numbers.metric-space-of-real-numbers
open import real-numbers.multiplication-real-numbers
open import real-numbers.multiplicative-inverses-nonzero-real-numbers
open import real-numbers.nonzero-real-numbers
open import real-numbers.powers-real-numbers
open import real-numbers.raising-universe-levels-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.series-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.strict-inequality-real-numbers
open import real-numbers.uniformly-continuous-functions-real-numbers

Idea

A geometric sequence of real numbers is a geometric sequence in the commutative ring of real numbers.

Definitions

geometric-sequence-ℝ : (l : Level) → UU (lsuc l)
geometric-sequence-ℝ l =
  geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)

seq-geometric-sequence-ℝ : {l : Level} → geometric-sequence-ℝ l → sequence (ℝ l)
seq-geometric-sequence-ℝ {l} =
  seq-geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)

standard-geometric-sequence-ℝ :
  {l : Level} → ℝ l → ℝ l → geometric-sequence-ℝ l
standard-geometric-sequence-ℝ {l} =
  standard-geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)

seq-standard-geometric-sequence-ℝ :
  {l : Level} → ℝ l → ℝ l → sequence (ℝ l)
seq-standard-geometric-sequence-ℝ {l} =
  seq-standard-geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)

Properties

The nth term of a geometric sequence with initial term a and common ratio r is a * rⁿ

module _
  {l : Level} (a r : ℝ l)
  where

  compute-standard-geometric-sequence-ℝ :
    (n : ℕ) → seq-standard-geometric-sequence-ℝ a r n ＝ a *ℝ power-ℝ n r
  compute-standard-geometric-sequence-ℝ n =
    inv
      ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
        ( commutative-ring-ℝ l)
        ( a)
        ( r)
        ( n))

If r is apart from 1, the sum of the first n elements of the standard geometric sequence n ↦ arⁿ is a(1-rⁿ)/(1-r)

sum-standard-geometric-fin-sequence-ℝ : {l : Level} → ℝ l → ℝ l → ℕ → ℝ l
sum-standard-geometric-fin-sequence-ℝ {l} =
  sum-standard-geometric-fin-sequence-Commutative-Ring (commutative-ring-ℝ l)

module _
  {l : Level} (a r : ℝ l) (r≠1 : apart-ℝ r one-ℝ)
  where

  abstract
    compute-sum-standard-geometric-fin-sequence-ℝ :
      (n : ℕ) →
      sum-standard-geometric-fin-sequence-ℝ a r n ＝
      ( ( a *ℝ
          real-inv-nonzero-ℝ
            ( nonzero-diff-apart-ℝ one-ℝ r (symmetric-apart-ℝ r≠1))) *ℝ
        (one-ℝ -ℝ power-ℝ n r))
    compute-sum-standard-geometric-fin-sequence-ℝ n =
      let
        1#r = symmetric-apart-ℝ r≠1
        1l#r =
          apart-left-sim-ℝ
            ( r)
            ( one-ℝ)
            ( raise-ℝ l one-ℝ)
            ( sim-raise-ℝ l one-ℝ)
            ( 1#r)
      in
        equational-reasoning
          sum-standard-geometric-fin-sequence-ℝ a r n
          ＝
            ( a *ℝ
              real-inv-nonzero-ℝ
                ( nonzero-diff-apart-ℝ (raise-ℝ l one-ℝ) r 1l#r)) *ℝ
            ( raise-ℝ l one-ℝ -ℝ power-ℝ n r)
            by
              compute-sum-standard-geometric-fin-sequence-Commutative-Ring
                ( commutative-ring-ℝ l)
                ( a)
                ( r)
                ( is-invertible-is-nonzero-ℝ _
                  ( is-nonzero-diff-is-apart-ℝ _ _ 1l#r))
                ( n)
          ＝
            ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-apart-ℝ one-ℝ r 1#r)) *ℝ
            ( one-ℝ -ℝ power-ℝ n r)
            by
              ap-mul-ℝ
                ( ap-mul-ℝ
                  ( refl)
                  ( ap
                    ( real-inv-nonzero-ℝ)
                    ( eq-nonzero-ℝ _ _
                      ( eq-sim-ℝ
                        ( preserves-sim-diff-ℝ
                          ( symmetric-sim-ℝ (sim-raise-ℝ l one-ℝ))
                          ( refl-sim-ℝ r))))))
                ( eq-sim-ℝ
                  ( preserves-sim-diff-ℝ
                    ( symmetric-sim-ℝ (sim-raise-ℝ l one-ℝ))
                    ( refl-sim-ℝ (power-ℝ n r))))

If |r| < 1, then the geometric series Σₙ arⁿ converges to a/(1-r)

This is the 66th theorem on Freek Wiedijk’s list of 100 theorems [Wie].

module _
  {l : Level} (a r : ℝ l)
  where

  standard-geometric-series-ℝ : series-ℝ l
  standard-geometric-series-ℝ =
    series-terms-ℝ (seq-standard-geometric-sequence-ℝ a r)

  abstract
    compute-sum-standard-geometric-series-ℝ :
      (|r|<1 : le-ℝ (abs-ℝ r) one-ℝ) →
      is-sum-series-ℝ
        ( standard-geometric-series-ℝ)
        ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1))
    compute-sum-standard-geometric-series-ℝ |r|<1 =
      let
        r#1 = apart-le-ℝ (concatenate-leq-le-ℝ _ _ _ (leq-abs-ℝ r) |r|<1)
      in
        binary-tr
          ( is-limit-sequence-ℝ)
          ( inv
            ( eq-htpy
              ( λ n →
                equational-reasoning
                  sum-standard-geometric-fin-sequence-ℝ a r n
                  ＝
                    ( a *ℝ real-inv-nonzero-ℝ _) *ℝ
                    ( one-ℝ -ℝ power-ℝ n r)
                    by compute-sum-standard-geometric-fin-sequence-ℝ a r r#1 n
                  ＝
                    ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ
                    ( one-ℝ -ℝ power-ℝ n r)
                    by
                      ap
                        ( λ z →
                          (a *ℝ real-inv-nonzero-ℝ z) *ℝ (one-ℝ -ℝ power-ℝ n r))
                        ( eq-nonzero-ℝ
                          ( nonzero-diff-apart-ℝ
                            ( one-ℝ)
                            ( r)
                            ( symmetric-apart-ℝ r#1))
                          ( nonzero-diff-le-abs-ℝ |r|<1)
                          ( refl)))))
          ( equational-reasoning
            ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ
            ( one-ℝ -ℝ raise-ℝ l zero-ℝ)
            ＝
              ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ
              ( one-ℝ -ℝ zero-ℝ)
              by
                eq-sim-ℝ
                  ( preserves-sim-left-mul-ℝ _ _ _
                    ( preserves-sim-diff-ℝ
                      ( refl-sim-ℝ one-ℝ)
                      ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))))
            ＝
              ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ one-ℝ
              by ap-mul-ℝ refl (right-unit-law-diff-ℝ one-ℝ)
            ＝ a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)
              by right-unit-law-mul-ℝ _)
          ( preserves-limits-sequence-uniformly-continuous-function-ℝ
            ( comp-uniformly-continuous-function-ℝ
              ( uniformly-continuous-right-mul-ℝ
                ( l)
                ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)))
              ( uniformly-continuous-diff-ℝ one-ℝ))
            ( λ n → power-ℝ n r)
            ( raise-ℝ l zero-ℝ)
            ( is-zero-lim-power-le-one-abs-ℝ r |r|<1))

References

[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes