[Merged by Bors] - feat(topology/algebra/ordered, topology/algebra/infinite_sum): bounded monotone sequences converge (variant versions) #7983
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hrmacbeth
added
the
awaiting-review
|
bors r+ |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jun 18, 2021
…d monotone sequences converge (variant versions) (#7983) A bounded monotone sequence converges to a value `a`, if and only if `a` is a least upper bound for its range. Mathlib had several variants of this fact previously (phrased in terms of, eg, `csupr`), but not quite this version (phrased in terms of `has_lub`). This version has a couple of advantages: - it applies to more general typeclasses (eg, `linear_order`) where the existence of suprema is not in general known - it applies to algebraic typeclasses (`linear_ordered_add_comm_monoid`, etc) where, since completeness of orders is not a mix-in, it is not possible to simultaneously assume `(conditionally_)complete_linear_order` The latter point makes these lemmas useful when dealing with `tsum`. We get: a nonnegative function `f` satisfies `has_sum f a`, if and only if `a` is a least upper bound for its partial sums.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A bounded monotone sequence converges to a value
a, if and only ifais a least upper bound for its range.Mathlib had several variants of this fact previously (phrased in terms of, eg,
csupr), but not quite this version (phrased in terms ofhas_lub). This version has a couple of advantages:linear_order) where the existence of suprema is not in general knownlinear_ordered_add_comm_monoid, etc) where, since completeness of orders is not a mix-in, it is not possible to simultaneously assume(conditionally_)complete_linear_orderThe latter point makes these lemmas useful when dealing with
tsum. We get: a nonnegative functionfsatisfieshas_sum f a, if and only ifais a least upper bound for its partial sums.Zulip