Open malarbol opened 4 months ago
Hello again. I've been playing around with metric structures and things like that. On the way I ended up needing/wanting these few new properties on sequences. They result interesting to prove things like ("asymptotical equality of sequences preserves limits", or "a sequence has a limit if and only of all its subsequence have this limit"). I think maybe these concepts could also prove themselves interesting in other contexts (e.g. polynomials on ring as asymptotically vanishing sequences, etc.).
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 @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 refactored a few concepts and cleaned things up a bit. I also updated the title/description of the PR to reflect better its content. If you prefer, maybe we could split this PR into two, with "new concepts" on one hand, and the "illustrative modules" on the other. Some of these modules could also be more interesting, like maybe proving that "decreasing sequences of natural numbers are asymptotically constant" is equivalent to the LPO, or study behavior of bounded increasing sequences of natural numbers but I'm not sure how to handle these right now.
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 :)
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 l
such thatA n
is pointed for sufficiently large natural numbersn
foundation.asymptotical-value-sequences
foundation.asymptotically-constant-sequences
:u
such thatu p = u q
for sufficiently largep
andq
foundation.asymptotically-equal-sequences
:u
andv
such thatu n = v n
for any sufficiently large natural numbern
foundation.constant-sequences
:foundation.subsequences
:u ∘ f
for some sequenceu
and 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-posets
Finally, 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.