Eventually pointed sequences

src/foundation.lagda.md

@@ -87,6 +87,7 @@ open import foundation.connected-components-universes public
 open import foundation.connected-maps public
 open import foundation.connected-types public
 open import foundation.constant-maps public
+open import foundation.constant-sequences public
 open import foundation.constant-span-diagrams public
 open import foundation.constant-type-families public
 open import foundation.continuations public
@@ -177,6 +178,9 @@ open import foundation.equivalences-span-diagrams-families-of-types public
 open import foundation.equivalences-spans public
 open import foundation.equivalences-spans-families-of-types public
 open import foundation.evaluation-functions public
+open import foundation.eventually-constant-sequences public
+open import foundation.eventually-equal-sequences public
+open import foundation.eventually-pointed-sequences-types public
 open import foundation.exclusive-disjunction public
 open import foundation.exclusive-sum public
 open import foundation.existential-quantification public

src/foundation/constant-sequences.lagda.md

@@ -0,0 +1,121 @@
+# Constant sequences
+
+```agda
+module foundation.constant-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.constant-maps
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.pi-decompositions
+open import foundation.sequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [sequence](foundation.sequences.md) `u` is
+{{#concept "constant" Disambiguation="sequence" Agda=is-constant-sequence}} if
+`u p ＝ u q` for all `p` and `q`.
+
+## Definitions
+
+### Constant sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-constant-sequence : UU l
+  is-constant-sequence = (p q : ℕ) → u p ＝ u q
+```
+
+### The type of constant sequences in a type
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  constant-sequence : UU l
+  constant-sequence = Σ (sequence A) is-constant-sequence
+```
+
+### Stationnary values of a sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-stationnary-value-sequence : ℕ → UU l
+  is-stationnary-value-sequence n = (u n) ＝ (u (succ-ℕ n))
+```
+
+## Properties
+
+### The value of a constant sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
+  where
+
+  value-constant-sequence : A
+  value-constant-sequence = u zero-ℕ
+
+  eq-value-constant-sequence : (n : ℕ) → value-constant-sequence ＝ u n
+  eq-value-constant-sequence = H zero-ℕ
+```
+
+### Constant sequences are constant
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A)
+  where
+
+  is-constant-const-sequence : is-constant-sequence (const ℕ x)
+  is-constant-const-sequence p q = refl
+```
+
+### A sequence is constant if all its terms are equal to some element
+
+```agda
+module _
+  {l : Level} {A : UU l} (x : A) (u : sequence A)
+  where
+
+  is-constant-htpy-constant-sequence :
+    (const ℕ x) ~ u → is-constant-sequence u
+  is-constant-htpy-constant-sequence H p q = inv (H p) ∙ H q
+```
+
+### A sequence is constant if and only if all its values are stationnary
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-stationnary-value-is-constant-sequence :
+    is-constant-sequence u → Π ℕ (is-stationnary-value-sequence u)
+  is-stationnary-value-is-constant-sequence H n = H n (succ-ℕ n)
+
+  is-constant-is-stationnary-value-sequence :
+    Π ℕ (is-stationnary-value-sequence u) → is-constant-sequence u
+  is-constant-is-stationnary-value-sequence H =
+    is-constant-htpy-constant-sequence
+      ( u zero-ℕ)
+      ( u)
+      ( ind-ℕ (refl) (λ n K → K ∙ H n))
+```

src/foundation/eventually-constant-sequences.lagda.md

@@ -0,0 +1,98 @@
+# Eventually constant sequences
+
+```agda
+module foundation.eventually-constant-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.constant-maps
+open import foundation.constant-sequences
+open import foundation.dependent-pair-types
+open import foundation.eventually-equal-sequences
+open import foundation.eventually-pointed-sequences-types
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [sequence](foundation.sequences.md) `u` is
+{{#concept "eventually constant" Disambiguation="sequence" Agda=is-eventually-constant-sequence}}
+if `u p ＝ u q` for sufficiently large `p` and `q`.
+
+## Definitions
+
+### Eventually constant sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u : sequence A)
+  where
+
+  is-eventually-constant-sequence : UU l
+  is-eventually-constant-sequence =
+    is-eventually-pointed-sequence
+      (λ p → is-eventually-pointed-sequence (λ q → u p ＝ u q))
+```
+
+### The eventual value of an eventually constant sequence
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H : is-eventually-constant-sequence u)
+  where
+
+  value-is-eventually-constant-sequence : A
+  value-is-eventually-constant-sequence =
+    u (modulus-is-eventually-pointed-sequence H)
+
+  is-eventual-value-is-eventually-constant-sequence :
+    is-eventually-pointed-sequence
+      (λ n → value-is-eventually-constant-sequence ＝ u n)
+  is-eventual-value-is-eventually-constant-sequence =
+    value-at-modulus-is-eventually-pointed-sequence H
+```
+
+## Properties
+
+### Constant sequences are eventually constant
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A} (H : is-constant-sequence u)
+  where
+
+  is-eventually-constant-is-constant-sequence :
+    is-eventually-constant-sequence u
+  pr1 is-eventually-constant-is-constant-sequence = zero-ℕ
+  pr2 is-eventually-constant-is-constant-sequence p I = (zero-ℕ , λ q J → H p q)
+```
+
+### An eventually constant sequence is eventually equal to the constant sequence of its eventual value
+
+```agda
+module _
+  {l : Level} {A : UU l} {u : sequence A}
+  (H : is-eventually-constant-sequence u)
+  where
+
+  eventually-eq-value-is-eventually-constant-sequence :
+    eventually-eq-sequence
+      ( const ℕ (value-is-eventually-constant-sequence H))
+      ( u)
+  eventually-eq-value-is-eventually-constant-sequence =
+    is-eventual-value-is-eventually-constant-sequence H
+```

src/foundation/eventually-equal-sequences.lagda.md

@@ -0,0 +1,147 @@
+# Eventually equal sequences
+
+```agda
+module foundation.eventually-equal-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.eventually-pointed-sequences-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Two [sequences](foundation.sequences.md) `u` and `v` are
+{{#concept "eventually equal" Disambiguation="sequences" Agda=eventually-eq-sequence}}
+if `u n ＝ v n` for sufficiently large
+[natural numbers](elementary-number-theory.natural-numbers.md) `n : ℕ`.
+
+## Definitions
+
+### The relation of being eventually equal sequences
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  eventually-eq-sequence : UU l
+  eventually-eq-sequence = is-eventually-pointed-sequence (λ n → u n ＝ v n)
+```
+
+### Modulus of eventual equality
+
+```agda
+module _
+  {l : Level} {A : UU l} {u v : sequence A} (H : eventually-eq-sequence u v)
+  where
+
+  modulus-eventually-eq-sequence : ℕ
+  modulus-eventually-eq-sequence = pr1 H
+
+  is-modulus-eventually-eq-sequence :
+    (n : ℕ) → leq-ℕ modulus-eventually-eq-sequence n → u n ＝ v n
+  is-modulus-eventually-eq-sequence = pr2 H
+```
+
+## Properties
+
+### Any sequence is asymptotically equal to itself
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  refl-eventually-eq-sequence : (u : sequence A) → eventually-eq-sequence u u
+  pr1 (refl-eventually-eq-sequence u) = zero-ℕ
+  pr2 (refl-eventually-eq-sequence u) m H = refl
+```
+
+### Homotopic sequences are eventually equal
+
+```agda
+  eventually-eq-htpy-sequence :
+    {u v : sequence A} → (u ~ v) → eventually-eq-sequence u v
+  eventually-eq-htpy-sequence {u} {v} I = (zero-ℕ , λ n H → I n)
+```
+
+### Eventual equality is a symmetric relation
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v : sequence A)
+  where
+
+  symmetric-eventually-eq-sequence :
+    eventually-eq-sequence u v → eventually-eq-sequence v u
+  symmetric-eventually-eq-sequence =
+    map-Π-is-eventually-pointed-sequence (λ n → inv)
+
+module _
+  {l : Level} {A : UU l} {u v : sequence A}
+  where
+
+  inv-eventually-eq-sequence :
+    eventually-eq-sequence u v → eventually-eq-sequence v u
+  inv-eventually-eq-sequence = symmetric-eventually-eq-sequence u v
+```
+
+### Eventual equality is a transitive relation
+
+```agda
+module _
+  {l : Level} {A : UU l} (u v w : sequence A)
+  where
+
+  transitive-eventually-eq-sequence :
+    eventually-eq-sequence v w →
+    eventually-eq-sequence u v →
+    eventually-eq-sequence u w
+  transitive-eventually-eq-sequence =
+    map-binary-Π-is-eventually-pointed-sequence (λ n I J → J ∙ I)
+```
+
+### Conjugation of asymptotical equality
+
+```agda
+module _
+  {l : Level} {A : UU l} {u u' v v' : sequence A}
+  where
+
+  conjugate-eventually-eq-sequence :
+    eventually-eq-sequence u u' →
+    eventually-eq-sequence v v' →
+    eventually-eq-sequence u v →
+    eventually-eq-sequence u' v'
+  conjugate-eventually-eq-sequence H K I =
+    transitive-eventually-eq-sequence u' u v'
+      ( transitive-eventually-eq-sequence u v v' K I)
+      ( inv-eventually-eq-sequence H)
+
+  conjugate-eventually-eq-sequence' :
+    eventually-eq-sequence u u' →
+    eventually-eq-sequence v v' →
+    eventually-eq-sequence u' v' →
+    eventually-eq-sequence u v
+  conjugate-eventually-eq-sequence' H K I =
+    transitive-eventually-eq-sequence u u' v
+      ( transitive-eventually-eq-sequence u' v' v
+        (inv-eventually-eq-sequence K) I)
+      ( H)
+```