Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

subsequences and asymptotical properties #1139

Draft
wants to merge 70 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
70 commits
Select commit Hold shift + click to select a range
6a14c46
subsequences
malarbol May 16, 2024
144cfd2
asymptotical equality preserves asymptotical constant sequences
malarbol May 16, 2024
4960088
fix indent
malarbol May 16, 2024
1daaa94
fix typo
malarbol May 16, 2024
b4d8abb
fix typo
malarbol May 16, 2024
fd166d1
fix typo
malarbol May 16, 2024
6e7828f
fix typo
malarbol May 16, 2024
c9456f0
remove unused imports
malarbol May 16, 2024
9a5c4d7
functoriality of subsequences
malarbol May 18, 2024
e54cd0c
rename monotonic-sequences-natural-numbers
malarbol May 18, 2024
fe1669f
constant sequences
malarbol May 18, 2024
c41da7f
refactor using asymptotical dependent sequences
malarbol May 20, 2024
5993bc4
fix typo
malarbol May 21, 2024
38ceb04
asymptotically-map-dependent-sequence
malarbol May 21, 2024
a3ef71d
cleanup
malarbol May 21, 2024
0b7a9b0
characterisation of asymptotically constant sequences
malarbol May 21, 2024
8af986a
cleanup
malarbol May 21, 2024
c74742a
refactor
malarbol May 21, 2024
94b24f5
leq-(left|right)-max-N
malarbol May 21, 2024
8737a71
lemma monotonic sequences natural numbers
malarbol May 23, 2024
449f010
Merge branch 'master' into subsequences
malarbol May 24, 2024
e504583
refactor asymptotical properties monotonic sequences natural numbers
malarbol May 26, 2024
47388b2
cleanup
malarbol May 27, 2024
556b357
cleanup names
malarbol May 27, 2024
6f333c7
fix indent
malarbol May 27, 2024
ebae214
more asymptotical lemma
malarbol May 27, 2024
7b7e1ce
use `tot` instead of `rec-Σ`
malarbol May 27, 2024
234fb41
fix indent
malarbol May 27, 2024
7083da2
le-skip-ℕ
malarbol May 28, 2024
94ee7c4
use `map-right-unit-law-coproduct-is-empty`
malarbol May 28, 2024
ba6b602
refactor/cleanup
malarbol May 28, 2024
d644cf9
fix typos/headers
malarbol May 28, 2024
b31f3a8
fix typo
malarbol May 28, 2024
9ee5a07
fix name
malarbol May 28, 2024
b817ff1
stationnary intervals of decreasing sequences of natural numbers
malarbol May 31, 2024
ea777aa
Merge branch 'master' into subsequences
malarbol May 31, 2024
8169cda
lint
malarbol May 31, 2024
7a3f3e9
WIP sequences posets
malarbol May 31, 2024
463c427
refactor monotonic sequences posets
malarbol Jun 1, 2024
020b954
asymptotical inequality sequences posets
malarbol Jun 1, 2024
da95b0f
fix name
malarbol Jun 1, 2024
50cae56
refactor using map-asymptotically
malarbol Jun 1, 2024
a79ade5
asymptotical lemma
malarbol Jun 1, 2024
b213e76
fix typo
malarbol Jun 1, 2024
5aeb28d
guarded asymptotical lemma sequences posets
malarbol Jun 1, 2024
7b08725
cleanup
malarbol Jun 1, 2024
7c16424
WIP cleanup
malarbol Jun 4, 2024
c646587
paren
malarbol Jun 5, 2024
a53663f
fix name and cleanup
malarbol Jun 5, 2024
605bf17
fix paren
malarbol Jun 5, 2024
711ebff
refactor and fix typo
malarbol Jun 5, 2024
78097dd
rename and add wikipedia ref
malarbol Jun 5, 2024
69855f6
fix name
malarbol Jun 5, 2024
119e759
fix typo
malarbol Jun 5, 2024
e3aafac
remove eq-sequence
malarbol Jun 5, 2024
21ca62e
remove unused import
malarbol Jun 5, 2024
b1c4164
fix typo
malarbol Jun 5, 2024
a21b400
refactor unbounded strict increasing sequencees
malarbol Jun 7, 2024
4e47e01
refactor strict-monotonic-sequences-natural-numbers
malarbol Jun 7, 2024
b216935
fix typo
malarbol Jun 7, 2024
282c311
cleanup
malarbol Jun 7, 2024
a7b9a55
refactor asymptotical value sequences
malarbol Jun 10, 2024
f5dad80
cleanup
malarbol Jun 10, 2024
ffc3d69
Merge branch 'master' into subsequences
malarbol Jun 10, 2024
c548823
refactor monotonic sequences
malarbol Jun 10, 2024
da70318
use preserves-order-Poset
malarbol Jun 10, 2024
43434a9
cleanup
malarbol Jun 11, 2024
92c431a
fix typo
malarbol Jun 11, 2024
23c2f9f
cleanup
malarbol Jun 11, 2024
17deaa9
cleanup
malarbol Jun 13, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
characterisation of asymptotically constant sequences
malarbol committed May 21, 2024
commit 0b7a9b0667bd1bc5601cd621c8c3abb6d9d17a99
165 changes: 153 additions & 12 deletions src/foundation/asymptotically-constant-sequences.lagda.md
Original file line number Diff line number Diff line change
@@ -7,7 +7,9 @@ module foundation.asymptotically-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.monotonic-sequences-natural-numbers
open import elementary-number-theory.natural-numbers

@@ -77,7 +79,51 @@ module _

is-∞-constant-is-constant-sequence : is-∞-constant-sequence u
pr1 is-∞-constant-is-constant-sequence = zero-ℕ
pr2 is-∞-constant-is-constant-sequence p I = zero-ℕ , λ q J → H p q
pr2 is-∞-constant-is-constant-sequence p I = (zero-ℕ , λ q J → H p q)
```

### The asymptotical value of an asymptotically constant sequence is unique

```agda
module _
{l : Level} {A : UU l} {u : sequence A}
(H K : is-∞-constant-sequence u)
where

all-equal-∞-value-∞-constant-sequence :
∞-value-∞-constant-sequence H = ∞-value-∞-constant-sequence K
all-equal-∞-value-∞-constant-sequence =
( is-modulus-∞-value-∞-constant-sequence
( H)
( max-ℕ
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K))
( leq-left-leq-max-ℕ
( max-ℕ
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K))
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K)
( refl-leq-ℕ
( max-ℕ
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K))))) ∙
( inv
( is-modulus-∞-value-∞-constant-sequence
( K)
( max-ℕ
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K))
( leq-right-leq-max-ℕ
( max-ℕ
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K))
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K)
( refl-leq-ℕ
( max-ℕ
( modulus-∞-value-∞-constant-sequence H)
( modulus-∞-value-∞-constant-sequence K))))))
```

### An asymptotically constant sequence is asymptotically equal to the constant sequence of its asymptotical value
@@ -98,7 +144,7 @@ module _

```agda
module _
{l : Level} {A : UU l} (u : sequence A) (x : A)
{l : Level} {A : UU l} (x : A) (u : sequence A)
where

is-∞-constant-eq-∞-constant-sequence :
@@ -120,20 +166,28 @@ module _
{l : Level} {A : UU l} (u : sequence A) (v : subsequence u)
where

eq-∞-value-∞-constant-subsequence :
(H : is-∞-constant-sequence u) →
eq-∞-sequence
( const-sequence (∞-value-∞-constant-sequence H))
( sequence-subsequence u v)
eq-∞-value-∞-constant-subsequence H =
( ( modulus-subsequence u v (modulus-∞-value-∞-constant-sequence H)) ,
( λ n I →
is-modulus-∞-value-∞-constant-sequence H
( extract-subsequence u v n)
( is-modulus-subsequence u v
( modulus-∞-value-∞-constant-sequence H)
( n)
( I))))

is-∞-constant-subsequence :
is-∞-constant-sequence u → is-∞-constant-sequence (sequence-subsequence u v)
is-∞-constant-subsequence H =
is-∞-constant-eq-∞-constant-sequence
( sequence-subsequence u v)
( ∞-value-∞-constant-sequence H)
( ( modulus-subsequence u v (modulus-∞-value-∞-constant-sequence H)) ,
( λ n I →
is-modulus-∞-value-∞-constant-sequence H
( extract-subsequence u v n)
( is-modulus-subsequence u v
( modulus-∞-value-∞-constant-sequence H)
( n)
( I))))
( sequence-subsequence u v)
( eq-∞-value-∞-constant-subsequence H)
```

### A sequence is asymptotically constant if all its subsequences are asymptotically constant
@@ -158,12 +212,99 @@ module _
preserves-∞-constant-eq-∞-sequence :
is-∞-constant-sequence u → is-∞-constant-sequence v
preserves-∞-constant-eq-∞-sequence K =
is-∞-constant-eq-∞-constant-sequence v
is-∞-constant-eq-∞-constant-sequence
( ∞-value-∞-constant-sequence K)
( v)
( transitive-eq-∞-sequence
( const-sequence (∞-value-∞-constant-sequence K))
( u)
( v)
( H)
( eq-∞-value-∞-constant-sequence K))
```

### Asymptotically stationnary sequences

#### The type of being asymptotically stationnary

```agda
module _
{l : Level} {A : UU l} (u : sequence A)
where

is-∞-stationnary-sequence : UU l
is-∞-stationnary-sequence = asymptotically (λ n → u n = u (succ-ℕ n))

is-∞-constant-modulus-is-∞-stationnary-sequence :
(H : is-∞-stationnary-sequence) →
(n : ℕ) →
leq-ℕ (modulus-∞-asymptotically H) n →
u (modulus-∞-asymptotically H) = u n
is-∞-constant-modulus-is-∞-stationnary-sequence H =
based-ind-ℕ
( modulus-∞-asymptotically H)
( λ n → u (modulus-∞-asymptotically H) = u n)
( refl)
( λ n I K → K ∙ is-modulus-∞-asymptotically H n I)
```

#### A sequence is asymptotically constant if and only if it is asymptotically stationnary

```agda
module _
{l : Level} {A : UU l} (u : sequence A)
where

is-∞-constant-is-∞-stationnary :
is-∞-stationnary-sequence u → is-∞-constant-sequence u
is-∞-constant-is-∞-stationnary H =
is-∞-constant-eq-∞-constant-sequence
( u (modulus-∞-asymptotically H))
( u)
( ( modulus-∞-asymptotically H) ,
( is-∞-constant-modulus-is-∞-stationnary-sequence u H))

is-∞-stationnary-is-∞-constant-sequence :
is-∞-constant-sequence u → is-∞-stationnary-sequence u
is-∞-stationnary-is-∞-constant-sequence H =
( ( modulus-∞-value-∞-constant-sequence H) ,
( λ n I →
( inv (is-modulus-∞-value-∞-constant-sequence H n I)) ∙
( is-modulus-∞-value-∞-constant-sequence
( H)
( succ-ℕ n)
( preserves-leq-succ-ℕ
( modulus-∞-value-∞-constant-sequence H)
( n)
( I)))))
```

### A sequence is asymptotically constant if and only if it is asymptotically equal to all its subsequences

```agda
module _
{l : Level} {A : UU l} (u : sequence A)
where

eq-∞-subsequence-is-∞-constant-sequence :
is-∞-constant-sequence u →
((v : subsequence u) → eq-∞-sequence u (sequence-subsequence u v))
eq-∞-subsequence-is-∞-constant-sequence H v =
transitive-eq-∞-sequence
( u)
( const-sequence (∞-value-∞-constant-sequence H))
( sequence-subsequence u v)
( eq-∞-value-∞-constant-subsequence u v H)
( symmetric-eq-∞-sequence
( const-sequence (∞-value-∞-constant-sequence H))
( u)
( eq-∞-value-∞-constant-sequence H))

is-∞-constant-eq-∞-sequence-subsequence :
((v : subsequence u) → eq-∞-sequence u (sequence-subsequence u v)) →
is-∞-constant-sequence u
is-∞-constant-eq-∞-sequence-subsequence H =
is-∞-constant-is-∞-stationnary
( u)
( H (skip-zero-sequence u))
```
15 changes: 15 additions & 0 deletions src/foundation/subsequences.lagda.md
Original file line number Diff line number Diff line change
@@ -64,6 +64,21 @@ module _

## Properties

### The subsequence that skips the first term

```agda
module _
{l : Level} {A : UU l} (u : sequence A)
where

skip-zero-sequence : subsequence u
skip-zero-sequence = (succ-ℕ , λ i j K → K)

eq-skip-zero-sequence :
(n : ℕ) → sequence-subsequence u skip-zero-sequence n = u (succ-ℕ n)
eq-skip-zero-sequence n = refl
```

### Any sequence is a subsequence of itself

```agda