subsequences and asymptotical properties #1139
Conversation
|
Hello again. |
|
Hey @malarbol, I'm just having a quick look at your changes for now, but why not have separate files for increasing and decreasing sequences? I would similarly expect us to have separate files for order-preserving and order-reversing maps |
Hey @fredrik-bakke, thanks for the feedback. I'm sorry, this PR got a bit bigger than anticipated (again 😅) and I still have a lot of cleanup to do. I'll do my best to address your concern; we may still need a module importing both of them, for properties like "a sequence is constant iff it is both increasing and decreasing". |
|
That's okay. The property you mentioned should go in a file abour constant sequences :) |
|
Hey again @fredrik-bakke. I already have a few follow-up ideas that motivated this PR:
|
|
Hey Malarbol! I'm back. Sorry for the terribly long wait; I'll try to review your PR in one of the coming days :) |
There was a problem hiding this comment.
After a preliminary review I've found a few deficiencies and conflicts with our style guide that should be corrected before I'm willing to take a closer look. Let me know when you've addressed my comments or if you have any questions regarding my comments. In the meanwhile I'll flag this PR as a draft again.
|
|
||
| ## Idea | ||
|
|
||
| A sequence of natural numbers is **decreasing** if it reverses |
There was a problem hiding this comment.
| A sequence of natural numbers is **decreasing** if it reverses | |
| A [sequence](foundation.sequences.md) of [natural numbers](elementary-number-theory.natural-numbers.md) is {{#concept "decreasing" Disambiguation="sequence of natural numbers" Agda=is-decreasing-sequence-ℕ}} if it reverses |
|
|
||
| ## Idea | ||
|
|
||
| A dependent sequence `A : ℕ → UU l` is **asymptotical** if `A n` is pointed for |
There was a problem hiding this comment.
If you have a dependent sequence a of A : ℕ → UU l then isn't every A n inhabited by a n? The sequence A : ℕ → UU l itself isn't dependent.
| A dependent sequence `A : ℕ → UU l` is **asymptotical** if `A n` is pointed for | ||
| sufficiently large natural numbers `n`. |
There was a problem hiding this comment.
Is "asymptotical sequence" standard terminology? I can't say I have heard it before. Would better terminology be "asymptotically pointed sequence of types"?
| A sequence `u` in a type `A` has an **asymptotical value** `x : A` if `x ＝ u n` | ||
| for sufficiently large natural numbers `n`. |
There was a problem hiding this comment.
Please add links to the concepts and use the {{#concept ...}} macro. this applies to all of your new files.
| ### Values of a sequence | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l : Level} {A : UU l} | ||
| where | ||
|
|
||
| is-value-sequence : A → sequence A → ℕ → UU l | ||
| is-value-sequence x u n = x ＝ u n | ||
| ``` |
There was a problem hiding this comment.
I'm not sure this definition is aiding readability, perhaps it is better to just write out x ＝ u n?
| asymptotically : UU l | ||
| asymptotically = Σ ℕ is-modulus-dependent-sequence |
There was a problem hiding this comment.
While I can appreciate that this definition makes some of your other code readable and intuitive once you know what it means, I can't say that this name should be reserved for this definition. Two questions I have immediately are
- why would you reserve asymptotics for sequences only over natural numbers
- shouldn't "asymptotically" be a property? If I say something holds asymptotically, would you expect it to matter how it holds asymptotically?
|
|
||
| ## Definitions | ||
|
|
||
| ### Asymptotical values of sequences |
There was a problem hiding this comment.
| ### Asymptotical values of sequences | |
| ### The Asymptotic value of an asymptotic sequence |
| is-∞-value-sequence : UU l | ||
| is-∞-value-sequence = asymptotically (is-value-sequence x u) |
There was a problem hiding this comment.
We avoid using unicode characters like ∞ in entry names except for in select rare cases like the namespace for the natural numbers ℕ. A better name for this entry would be takes-value-asymptotically or value-at-infinity-equals
| @@ -0,0 +1,123 @@ | |||
| # Asymptotical value of a sequence | |||
There was a problem hiding this comment.
Isn't "asymptotic" the correct conjugation of the word? Please check and if so review your contribution to reflect the correct conjugation
| is-strict-increasing-prop-sequence-ℕ : Prop lzero | ||
| is-strict-increasing-prop-sequence-ℕ = | ||
| Π-Prop ℕ | ||
| ( λ i → | ||
| Π-Prop ℕ | ||
| ( λ j → hom-Prop (le-ℕ-Prop i j) (le-ℕ-Prop (f i) (f j)))) |
There was a problem hiding this comment.
It's more appropriate to define strictly increasing sequences as order homomorphisms of the strict ordering on the natural numbers.
| is-strict-increasing-prop-sequence-ℕ : Prop lzero | ||
| is-strict-increasing-prop-sequence-ℕ = |
There was a problem hiding this comment.
This should be named is-strictly-increasing-...
| is-strict-decreasing-sequence-ℕ : UU lzero | ||
| is-strict-decreasing-sequence-ℕ = | ||
| (i j : ℕ) → le-ℕ i j → le-ℕ (f j) (f i) |
There was a problem hiding this comment.
this should be named is-strictly-decreasing-...
This pull request introduces the concept of subsequence of a sequence and asymptotical behavior of sequences.
In addition, we introduce a few illustrative results using these concepts on sequences in partially ordered sets and monotonic sequences of natural numbers.
More precisely, we introduce the following concepts:
elementary-number-theory.strictly-increasing-sequences-natural-numbers:f : ℕ → ℕthat preserve strict inequality of natural numberselementary-number-theory.strictly-decreasing-sequences-natural-numbers:f : ℕ → ℕthat reverse strict inequality of natural numbersfoundation.asymptotical-dependent-sequences:A : ℕ → UU lsuch thatA nis pointed for sufficiently large natural numbersnfoundation.asymptotical-value-sequencesfoundation.asymptotically-constant-sequences:usuch thatu p ＝ u qfor sufficiently largepandqfoundation.asymptotically-equal-sequences:uandvsuch thatu n ＝ v nfor any sufficiently large natural numbernfoundation.constant-sequences:foundation.subsequences:u ∘ ffor some sequenceuand strictly increasing mapf : ℕ → ℕThese concepts are used in the following modules to serve as illustrative examples
elementary-number-theory.decreasing-sequences-natural-numbers:elementary-number-theory.increasing-sequences-natural-numbers:order-theory.constant-sequences-posets:order-theory.decreasing-sequences-posets:order-theory.increasing-sequences-posets:order-theory.monotonic-sequences-posets:order-theory.sequences-posetsFinally, we also introduce a few helpful properties on existing concepts, e.g. "the maximum of two natural numbers is greater than each of them", "two equal elements in a poset are comparable", etc.