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
[Merged by Bors] - feat(analysis): Cauchy sequence and series lemmas #7858
Conversation
from LTE. Mostly relaxing assumptions from metric to pseudo-metric and priving some obvious lemmas.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Is it reasonable to have something like |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
src/analysis/specific_limits.lean
Outdated
variables [semi_normed_group α] {r C : ℝ} {f : ℕ → α} | ||
|
||
lemma normed_group.cauchy_seq_of_le_geometric {C : ℝ} {r : ℝ} (hr : r < 1) | ||
{u : ℕ → α} (h : ∀ n, ∥u n - u (n + 1)∥ ≤ C*r^n) : cauchy_seq u := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
{u : ℕ → α} (h : ∀ n, ∥u n - u (n + 1)∥ ≤ C*r^n) : cauchy_seq u := | |
{u : ℕ → α} (h : ∀ n, ∥u n - u (n + 1)∥ ≤ C*r^n) : cauchy_seq u := |
end | ||
|
||
lemma normed_group.cauchy_series_of_le_geometric'' {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ} | ||
(hr₀ : 0 < r) (hr₁ : r < 1) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
hr₀
seems useless here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I got tired of lemmas where most of the proof deals with weakening such constraint whereas they are never an issue when applying the lemma. Look at the previous lemma. Most of the proof is showing we can assume C and r are positive.
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
from LTE. Mostly relaxing assumptions from metric to pseudo-metric and proving some obvious lemmas. eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`. In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.
Build failed (retrying...): |
from LTE. Mostly relaxing assumptions from metric to pseudo-metric and proving some obvious lemmas. eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`. In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.
This PR was included in a batch that was canceled, it will be automatically retried |
from LTE. Mostly relaxing assumptions from metric to pseudo-metric and proving some obvious lemmas. eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`. In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.
Build failed (retrying...): |
from LTE. Mostly relaxing assumptions from metric to pseudo-metric and proving some obvious lemmas. eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`. In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.
from LTE. Mostly relaxing assumptions from metric to pseudo-metric and proving some obvious lemmas. eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`. In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.
Pull request successfully merged into master. Build succeeded: |
from LTE. Mostly relaxing assumptions from metric to
pseudo-metric and proving some obvious lemmas.
eventually_constant_prod and eventually_constant_sum are duplicated by hand because
to_additive
gets confused by the appearance of1
.In
norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]
and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.