subsequences and asymptotical properties

[malarbol]

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:
  • sequences f : ℕ → ℕ that preserve strict inequality of natural numbers
  • basic properties
  • strictly increasing sequences of natural numbers take arbitrarily large values
• elementary-number-theory.strictly-decreasing-sequences-natural-numbers:
  • sequences f : ℕ → ℕ that reverse strict inequality of natural numbers
  • they do not exist
• foundation.asymptotical-dependent-sequences:
  • dependent sequences A : ℕ → UU l such that A n is pointed for sufficiently large natural numbers n
  • basic properties
  • asymptotical (binary) functoriality
• foundation.asymptotical-value-sequences
  • sequences that asymptotically take the same value
  • basic properties
• foundation.asymptotically-constant-sequences:
  • sequences u such that u p ＝ u q for sufficiently large p and q
  • a sequence is asymptotically constant if and only if it is asymptotically equal to a constant sequence
  • a sequence is asymptotically constant if and only if all its subsequences are asymptotically constant
  • a sequence asymptotically equal to an asymptotically constant sequence is asymptotically constant
  • characterization as asymptotically stationary sequences
  • a sequence is asymptotically constant if and only if it is asymptotically equal to all its subsequences
• foundation.asymptotically-equal-sequences:
  • sequences u and v such that u n ＝ v n for any sufficiently large natural number n
  • reflexivity, symmetry, transitivity
• foundation.constant-sequences:
  • sequences for which all terms are equal
  • basic properties
• foundation.subsequences:
  • sequences u ∘ f for some sequence u and strictly increasing map f : ℕ → ℕ
  • properties
    • any sequence is a subsequence of itself
    • a subsequence of a subsequence is a subsequence if the original sequence
    • subsequences are functorial
    • a dependent sequence is asymptotical if and only if all its subsequences are asymptotical

These concepts are used in the following modules to serve as illustrative examples

• elementary-number-theory.decreasing-sequences-natural-numbers:
  • sequences of natural numbers that reverse inequality
  • a few conditions under which a decreasing sequence of natural numbers is asymptotically constant
• elementary-number-theory.increasing-sequences-natural-numbers:
  • sequences of natural numbers that preserve inequality
• order-theory.constant-sequences-posets:
  • characterization as increasing and decreasing sequences
• order-theory.decreasing-sequences-posets:
  • sequences in partially ordered sets that reverse the ordering
  • properties
  • sub-sequential properties
  • a few conditions under which a decreasing sequence is asymptotically constant
• order-theory.increasing-sequences-posets:
  • sequences in partially ordered sets that preserve the ordering
  • properties
  • sub-sequential properties
  • a few conditions under which an increasing sequence is asymptotically constant
• order-theory.monotonic-sequences-posets:
  • a decreasing/increasing sequence is asymptotically constant if it has an increasing/decreasing subsequence
• order-theory.sequences-posets
  • sequences in the underlying type of a partially ordered set
  • comparison of sequences in a partially ordered set
  • asymptotical comparison of sequences in a partially ordered set
  • a sequence asymptotically between to asymptotical sequences is asymptotically equal to them

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.

[malarbol]

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.).

[fredrik-bakke]

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

[malarbol]

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".

[fredrik-bakke]

That's okay. The property you mentioned should go in a file abour constant sequences :)

[malarbol]

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:

• metric structures (with sequential limits, etc.)
• series, polynomials, convolution products, etc. (using asymptotically vanishing sequence in monoids, rings, etc.)

[fredrik-bakke]

Hey Malarbol! I'm back. Sorry for the terribly long wait; I'll try to review your PR in one of the coming days :)

[fredrik-bakke]

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.

[fredrik-bakke]

Suggested change

	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

[fredrik-bakke]

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.

[fredrik-bakke]

Is "asymptotical sequence" standard terminology? I can't say I have heard it before. Would better terminology be "asymptotically pointed sequence of types"?

[fredrik-bakke]

Please add links to the concepts and use the {{#concept ...}} macro. this applies to all of your new files.

[fredrik-bakke]

I'm not sure this definition is aiding readability, perhaps it is better to just write out x ＝ u n?

[fredrik-bakke]

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?

[fredrik-bakke]

Suggested change

	### Asymptotical values of sequences
	### The Asymptotic value of an asymptotic sequence

[fredrik-bakke]

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

[fredrik-bakke]

Isn't "asymptotic" the correct conjugation of the word? Please check and if so review your contribution to reflect the correct conjugation

[fredrik-bakke]

It's more appropriate to define strictly increasing sequences as order homomorphisms of the strict ordering on the natural numbers.

[fredrik-bakke]

This should be named is-strictly-increasing-...

[fredrik-bakke]

this should be named is-strictly-decreasing-...

[fredrik-bakke]

I'm closing this PR as it seems to have been abandoned. I'll note that the work that is done here seems highly relevant to #1211 perhaps some of this work can be salvaged @EgbertRijke?

[fredrik-bakke]

Also, feel free to reopen at any point @malarbol, your contributions are most welcome!

[malarbol]

I'm closing this PR as it seems to have been abandoned. I'll note that the work that is done here seems highly relevant to #1211 perhaps some of this work can be salvaged @EgbertRijke?

Hey @fredrik-bakke! I've been wanted to get in touch for some months now but I couldn't find the time / courage / motivation, etc. I'm quite sorry. I've been busy with work, and other side-projects and I haven't written any agda since my PR on metric spaces. But I do miss it so I might get back to it sometimes soon.

I should have closed this PR for month. I opened it to share some of my thoughts around convergence / asymptotical behavior but that was never really ready to be merged. Obviously, feel free to salvage anything you find interesting. Or we can talk about it and restart it from scratch with a better setting.

Also, feel free to reopen at any point @malarbol, your contributions are most welcome!

Or I'll reopen it if I manage to clean it up. We'll see.

I see there's been a lot of contributions in the real-numbers module, that's really nice! I'll have to read it carefully but it's already giving me some ideas. Is anybody working towards Cauchy-completeness of the real numbers? It seems that the recent additions on the density of Q in R was the missing piece to link real numbers and rational Cauchy approximations.

Take care.
I look forward to contribute again.

PS: is there any feedback on the metric-spaces module? People complaining about the name scheme or coming up with better ideas? I feel like I told you I would think about it and fix the names, and never really did it. Sorry.

[fredrik-bakke]

Hey, it's nice to hear from you again! I've tried to get in touch a couple of times via Discord, don't hesitate to contact me there whenever you feel like it. I'm sorry to hear about your lacking courage and motivation, it would indeed be great to have you back!

Regarding real-numbers, yes, we have a new contributor who's picked up the torch. It's possible he might be going for that although I'm not sure. If you want to get in touch with them I can give you their contact details in private, or you can get in touch with him here.

I think your metric-space module turned out great! There are maybe some minor naming changes I'd personally like to see, but there's nothing pressing, and the names can always be changed later. I'm way too opinionated on naming at times anyway, so you shouldn't worry too much about it.

Hope to hear from you again soon!