Sequences of positive rational numbers

src/elementary-number-theory.lagda.md

@@ -23,9 +23,11 @@ open import elementary-number-theory.archimedean-property-natural-numbers public
 open import elementary-number-theory.archimedean-property-positive-rational-numbers public
 open import elementary-number-theory.archimedean-property-rational-numbers public
 open import elementary-number-theory.arithmetic-functions public
+open import elementary-number-theory.arithmetic-sequences-positive-rational-numbers public
 open import elementary-number-theory.based-induction-natural-numbers public
 open import elementary-number-theory.based-strong-induction-natural-numbers public
 open import elementary-number-theory.bell-numbers public
+open import elementary-number-theory.bernoullis-inequality-positive-rational-numbers public
 open import elementary-number-theory.bezouts-lemma-integers public
 open import elementary-number-theory.bezouts-lemma-natural-numbers public
 open import elementary-number-theory.binomial-coefficients public
@@ -74,6 +76,7 @@ open import elementary-number-theory.field-of-rational-numbers public
 open import elementary-number-theory.finitary-natural-numbers public
 open import elementary-number-theory.finitely-cyclic-maps public
 open import elementary-number-theory.fundamental-theorem-of-arithmetic public
+open import elementary-number-theory.geometric-sequences-positive-rational-numbers public
 open import elementary-number-theory.goldbach-conjecture public
 open import elementary-number-theory.greatest-common-divisor-integers public
 open import elementary-number-theory.greatest-common-divisor-natural-numbers public

src/elementary-number-theory/addition-rational-numbers.lagda.md

@@ -13,6 +13,7 @@ open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-integers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.reduced-integer-fractions
 
@@ -276,6 +277,15 @@ abstract
   succ-rational-ℤ = add-rational-ℤ one-ℤ
 ```
 
+### The rational successor of a natural number is the successor of the natural number
+
+```agda
+abstract
+  succ-rational-ℕ : (x : ℕ) → succ-ℚ (rational-ℕ x) ＝ rational-ℕ (succ-ℕ x)
+  succ-rational-ℕ x =
+    succ-rational-ℤ (int-ℕ x) ∙ ap rational-ℤ (succ-int-ℕ x)
+```
+
 ## See also
 
 - The additive group structure on the rational numbers is defined in

src/elementary-number-theory/arithmetic-sequences-positive-rational-numbers.lagda.md

@@ -0,0 +1,309 @@
+# Arithmetic sequences of positive rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.arithmetic-sequences-positive-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.archimedean-property-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.arithmetic-sequences-semigroups
+open import group-theory.powers-of-elements-monoids
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "arithmetic sequence" Disambiguation="of positive rational numbers" Agda=arithmetic-sequence-ℚ⁺ WD="arithmetic progression" WDID=Q170008}}
+of positive rational numbers is an
+[arithmetic sequence](group-theory.arithmetic-sequences-semigroups.md) in the
+additive [semigroup](group-theory.semigroups.md) of
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md).
+
+The values of an arithmetic sequence are determined by its initial value and its
+common difference; an arithmetic sequence of positive rational numbers is
+strictly increasing and unbounded.
+
+## Definitions
+
+### Arithmetic sequences of positive rational numbers
+
+```agda
+is-common-difference-sequence-ℚ⁺ : sequence ℚ⁺ → ℚ⁺ → UU lzero
+is-common-difference-sequence-ℚ⁺ =
+  is-common-difference-sequence-Semigroup semigroup-add-ℚ⁺
+
+is-arithmetic-sequence-ℚ⁺ : sequence ℚ⁺ → UU lzero
+is-arithmetic-sequence-ℚ⁺ =
+  is-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺
+
+arithmetic-sequence-ℚ⁺ : UU lzero
+arithmetic-sequence-ℚ⁺ = arithmetic-sequence-Semigroup semigroup-add-ℚ⁺
+
+module _
+  (u : arithmetic-sequence-ℚ⁺)
+  where
+
+  seq-arithmetic-sequence-ℚ⁺ : sequence ℚ⁺
+  seq-arithmetic-sequence-ℚ⁺ =
+    seq-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺ u
+
+  is-arithmetic-seq-arithmetic-sequence-ℚ⁺ :
+    is-arithmetic-sequence-Semigroup
+      semigroup-add-ℚ⁺
+      seq-arithmetic-sequence-ℚ⁺
+  is-arithmetic-seq-arithmetic-sequence-ℚ⁺ =
+    is-arithmetic-seq-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺ u
+
+  common-difference-arithmetic-sequence-ℚ⁺ : ℚ⁺
+  common-difference-arithmetic-sequence-ℚ⁺ =
+    common-difference-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺ u
+
+  is-common-difference-arithmetic-sequence-ℚ⁺ :
+    is-common-difference-sequence-Semigroup
+      semigroup-add-ℚ⁺
+      seq-arithmetic-sequence-ℚ⁺
+      common-difference-arithmetic-sequence-ℚ⁺
+  is-common-difference-arithmetic-sequence-ℚ⁺ =
+    is-common-difference-arithmetic-sequence-Semigroup
+      semigroup-add-ℚ⁺
+      u
+
+  init-term-arithmetic-sequence-ℚ⁺ : ℚ⁺
+  init-term-arithmetic-sequence-ℚ⁺ =
+    init-term-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺ u
+```
+
+### The standard arithmetic sequence of positive rational numbers with initial term `a` and common difference `d`
+
+```agda
+module _
+  (a d : ℚ⁺)
+  where
+
+  standard-arithmetic-sequence-ℚ⁺ : arithmetic-sequence-ℚ⁺
+  standard-arithmetic-sequence-ℚ⁺ =
+    standard-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺ a d
+
+  seq-standard-arithmetic-sequence-ℚ⁺ : sequence ℚ⁺
+  seq-standard-arithmetic-sequence-ℚ⁺ =
+    seq-arithmetic-sequence-ℚ⁺ standard-arithmetic-sequence-ℚ⁺
+```
+
+## Properties
+
+### Two arithmetic sequences of positive rational numbers with the same initial term and common difference are homotopic
+
+```agda
+htpy-seq-arithmetic-sequence-ℚ⁺ :
+  ( u v : arithmetic-sequence-ℚ⁺) →
+  ( eq-init :
+    init-term-arithmetic-sequence-ℚ⁺ u ＝
+    init-term-arithmetic-sequence-ℚ⁺ v) →
+  ( eq-common-difference :
+    common-difference-arithmetic-sequence-ℚ⁺ u ＝
+    common-difference-arithmetic-sequence-ℚ⁺ v) →
+  seq-arithmetic-sequence-ℚ⁺ u ~ seq-arithmetic-sequence-ℚ⁺ v
+htpy-seq-arithmetic-sequence-ℚ⁺ =
+  htpy-seq-arithmetic-sequence-Semigroup semigroup-add-ℚ⁺
+```
+
+### The nth term of the arithmetic sequence with initial term `a` and common difference `d` is `a + n d`
+
+```agda
+module _
+  (a d : ℚ⁺)
+  where
+
+  abstract
+    compute-standard-arithmetic-sequence-ℚ⁺ :
+      ( n : ℕ) →
+      ( rational-ℚ⁺ a +ℚ rational-ℕ n *ℚ rational-ℚ⁺ d) ＝
+      ( rational-ℚ⁺ (seq-standard-arithmetic-sequence-ℚ⁺ a d n))
+    compute-standard-arithmetic-sequence-ℚ⁺ zero-ℕ =
+      ( ap (add-ℚ (rational-ℚ⁺ a)) (left-zero-law-mul-ℚ (rational-ℚ⁺ d))) ∙
+      ( right-unit-law-add-ℚ (rational-ℚ⁺ a))
+    compute-standard-arithmetic-sequence-ℚ⁺ (succ-ℕ n) =
+      ( ap
+        ( add-ℚ (rational-ℚ⁺ a))
+        ( ( α n (rational-ℚ⁺ d))) ∙
+          ( inv
+            ( associative-add-ℚ
+              ( rational-ℚ⁺ a)
+              ( rational-ℕ n *ℚ rational-ℚ⁺ d)
+              ( rational-ℚ⁺ d))) ∙
+          ( ap
+            ( add-ℚ' (rational-ℚ⁺ d))
+            ( compute-standard-arithmetic-sequence-ℚ⁺ n)))
+      where
+
+        α :
+          (m : ℕ) (q : ℚ) →
+          (rational-ℕ (succ-ℕ m) *ℚ q) ＝ (rational-ℕ m) *ℚ q +ℚ q
+        α m q =
+          ( ap
+            ( mul-ℚ' q)
+            ( ( inv (succ-rational-ℕ m)) ∙
+              ( commutative-add-ℚ one-ℚ (rational-ℕ m)))) ∙
+          ( right-distributive-mul-add-ℚ
+            ( rational-ℕ m)
+            ( one-ℚ)
+            ( q)) ∙
+          ( ap
+            ( add-ℚ (rational-ℕ m *ℚ q))
+            ( left-unit-law-mul-ℚ q))
+
+module _
+  (u : arithmetic-sequence-ℚ⁺)
+  where
+
+  abstract
+    compute-arithmetic-sequence-ℚ⁺ :
+      ( n : ℕ) →
+      Id
+        ( add-ℚ
+          ( rational-ℚ⁺ (init-term-arithmetic-sequence-ℚ⁺ u))
+          ( mul-ℚ
+            ( rational-ℕ n)
+            ( rational-ℚ⁺ (common-difference-arithmetic-sequence-ℚ⁺ u))))
+        ( rational-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u n))
+    compute-arithmetic-sequence-ℚ⁺ n =
+      ( compute-standard-arithmetic-sequence-ℚ⁺
+        ( init-term-arithmetic-sequence-ℚ⁺ u)
+        ( common-difference-arithmetic-sequence-ℚ⁺ u)
+        ( n)) ∙
+      ( ap
+        ( rational-ℚ⁺)
+        ( htpy-seq-standard-arithmetic-sequence-Semigroup
+          semigroup-add-ℚ⁺
+          u
+          n))
+```
+
+### An arithmetic sequence of positive rational numbers is strictly increasing
+
+```agda
+module _
+  (u : arithmetic-sequence-ℚ⁺) (n : ℕ)
+  where
+
+  abstract
+    is-strictly-increasing-arithmetic-sequence-ℚ⁺ :
+      le-ℚ⁺
+        ( seq-arithmetic-sequence-ℚ⁺ u n)
+        ( seq-arithmetic-sequence-ℚ⁺ u (succ-ℕ n))
+    is-strictly-increasing-arithmetic-sequence-ℚ⁺ =
+      inv-tr
+        ( le-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u n))
+        ( is-common-difference-arithmetic-sequence-ℚ⁺ u n)
+        ( le-right-add-rational-ℚ⁺
+          ( rational-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u n))
+          ( common-difference-arithmetic-sequence-ℚ⁺ u))
+```
+
+### The terms of an arithmetic sequence of positive rational numbers are greater than or equal to its initial term
+
+```agda
+module _
+  (u : arithmetic-sequence-ℚ⁺)
+  where
+
+  abstract
+    leq-init-arithmetic-sequence-ℚ⁺ :
+      (n : ℕ) →
+      leq-ℚ⁺
+        ( init-term-arithmetic-sequence-ℚ⁺ u)
+        ( seq-arithmetic-sequence-ℚ⁺ u n)
+    leq-init-arithmetic-sequence-ℚ⁺ zero-ℕ =
+      refl-leq-ℚ ( rational-ℚ⁺ (init-term-arithmetic-sequence-ℚ⁺ u))
+    leq-init-arithmetic-sequence-ℚ⁺ (succ-ℕ n) =
+      leq-le-ℚ
+      { rational-ℚ⁺ (init-term-arithmetic-sequence-ℚ⁺ u)}
+      { rational-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u (succ-ℕ n))}
+      ( concatenate-leq-le-ℚ
+        ( rational-ℚ⁺ (init-term-arithmetic-sequence-ℚ⁺ u))
+        ( rational-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u n))
+        ( rational-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u (succ-ℕ n)))
+        ( leq-init-arithmetic-sequence-ℚ⁺ n)
+        ( is-strictly-increasing-arithmetic-sequence-ℚ⁺ u n))
+```
+
+### An arithmetic sequence of positive rational numbers has no upper bound
+
+```agda
+module _
+  (u : arithmetic-sequence-ℚ⁺)
+  where
+
+  opaque
+    is-unbounded-arithmetic-sequence-ℚ⁺ :
+      (M : ℚ⁺) → Σ ℕ (le-ℚ⁺ M ∘ seq-arithmetic-sequence-ℚ⁺ u)
+    is-unbounded-arithmetic-sequence-ℚ⁺ M =
+      tot
+        ( tr-archimidean-bound)
+        ( bound-archimedean-property-ℚ
+          ( rational-ℚ⁺ (common-difference-arithmetic-sequence-ℚ⁺ u))
+          ( rational-ℚ⁺ M)
+          ( is-positive-rational-ℚ⁺
+            ( common-difference-arithmetic-sequence-ℚ⁺ u)))
+      where
+
+        tr-archimidean-bound :
+          (n : ℕ) →
+          (I :
+            le-ℚ
+              ( rational-ℚ⁺ M)
+              ( mul-ℚ
+                ( rational-ℕ n)
+                ( rational-ℚ⁺ (common-difference-arithmetic-sequence-ℚ⁺ u)))) →
+          le-ℚ⁺ M (seq-arithmetic-sequence-ℚ⁺ u n)
+        tr-archimidean-bound n =
+          transitive-le-ℚ
+            ( rational-ℚ⁺ M)
+            ( mul-ℚ
+              ( rational-ℕ n)
+              ( rational-ℚ⁺ (common-difference-arithmetic-sequence-ℚ⁺ u)))
+            ( rational-ℚ⁺ (seq-arithmetic-sequence-ℚ⁺ u n))
+            ( tr
+              ( le-ℚ
+                ( mul-ℚ
+                  ( rational-ℕ n)
+                  ( rational-ℚ⁺ (common-difference-arithmetic-sequence-ℚ⁺ u))))
+              ( compute-arithmetic-sequence-ℚ⁺ u n)
+              ( le-left-add-rational-ℚ⁺
+                ( mul-ℚ
+                  ( rational-ℕ n)
+                  ( rational-ℚ⁺ (common-difference-arithmetic-sequence-ℚ⁺ u)))
+                ( init-term-arithmetic-sequence-ℚ⁺ u)))
+```
+
+## References
+
+- [Arithmetic progressions](https://en.wikipedia.org/wiki/Arithmetic_progression)
+  at Wikipedia