Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(analysis/asymptotics): Equivalent definitions for is_[oO] u v l looking like u = φ * v for some φ #4646

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(analysis/asymptotics): Equivalent definitions for is_[oO] u v l looking like u = φ * v for some φ #4646

wants to merge 11 commits into from

Conversation

ADedecker
Copy link
Member

@ADedecker ADedecker commented Oct 16, 2020 •
edited by github-actions bot

The advantage of these statements over u/v tendsto 0 / is bounded is they do not require any nonvanishing assumptions about v

These are preliminaries for defining and proving basic lemmas about the "asymptotic equivalence" relation.

@ADedecker ADedecker added the awaiting-review The author would like community review of the PR label Oct 16, 2020
@PatrickMassot PatrickMassot added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 16, 2020
@ADedecker ADedecker added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 16, 2020
urkud
urkud reviewed Oct 18, 2020
View reviewed changes
Copy link
Member

@urkud urkud left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My laptop is currently half-broken, so I haven't tested any of the suggestions. Most of them are about using eventually.mono in more cases.

src/analysis/asymptotics.lean Outdated Show resolved Hide resolved
src/analysis/asymptotics.lean Outdated Show resolved Hide resolved
src/analysis/asymptotics.lean Outdated Show resolved Hide resolved
@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 18, 2020
@ADedecker ADedecker added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 23, 2020
ADedecker and others added 3 commits October 23, 2020 16:56
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 24, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 24, 2020
@urkud
Copy link
Member

urkud commented Oct 24, 2020

I'm sorry for adding unrelated material to the PR. I didn't think that adding these two @[simp]s will cause compile failures. Probably I should move this to another PR.

urkud added a commit that referenced this pull request Oct 24, 2020
@urkud
chore(algebra/group/pi): add pi.has_div
a819d1d 
Motivated by #4646
@urkud urkud mentioned this pull request Oct 24, 2020
Closed
@urkud urkud added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 24, 2020
bors bot pushed a commit that referenced this pull request Oct 25, 2020
@urkud
chore(algebra/group/pi): add pi.has_div (#4776)
14cff9a 
Motivated by #4646
@urkud urkud removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 26, 2020
@urkud @hrmacbeth
Apply suggestions from code review
a4163cf 
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
@hrmacbeth
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 30, 2020
bors bot pushed a commit that referenced this pull request Oct 30, 2020
@ADedecker @urkud
feat(analysis/asymptotics): Equivalent definitions for `is_[oO] u v l…
581b2af 
…` looking like `u = φ * v` for some `φ` (#4646)

The advantage of these statements over `u/v` tendsto 0 / is bounded is they do not require any nonvanishing assumptions about `v`



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link

bors bot commented Oct 30, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/asymptotics): Equivalent definitions for is_[oO] u v l looking like u = φ * v for some φ [Merged by Bors] - feat(analysis/asymptotics): Equivalent definitions for is_[oO] u v l looking like u = φ * v for some φ Oct 30, 2020
@bors bors bot closed this Oct 30, 2020
@bors bors bot deleted the is_oO_normed branch October 30, 2020 03:17
lecopivo pushed a commit to lecopivo/mathlib that referenced this pull request Oct 31, 2020
@ADedecker @urkud
feat(analysis/asymptotics): Equivalent definitions for `is_[oO] u v l…
85a0f8b 
…` looking like `u = φ * v` for some `φ` (leanprover-community#4646)

The advantage of these statements over `u/v` tendsto 0 / is bounded is they do not require any nonvanishing assumptions about `v`



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@PatrickMassot PatrickMassot PatrickMassot left review comments

@hrmacbeth hrmacbeth hrmacbeth left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@ADedecker @urkud @hrmacbeth @bryangingechen @PatrickMassot