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(dynamics/periodic_pts): Orbit under periodic function #12976

Closed
wants to merge 32 commits into from
Closed

[Merged by Bors] - feat(dynamics/periodic_pts): Orbit under periodic function #12976

wants to merge 32 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Mar 27, 2022 •
edited by github-actions bot

@vihdzp vihdzp added the awaiting-review The author would like community review of the PR label Mar 27, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Mar 27, 2022
@vihdzp vihdzp mentioned this pull request Mar 27, 2022
Closed
7 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Apr 1, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 1, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 2, 2022
ocfnash
ocfnash requested changes Apr 13, 2022
View reviewed changes
src/dynamics/periodic_pts.lean Outdated Show resolved Hide resolved
src/dynamics/periodic_pts.lean Outdated Show resolved Hide resolved
src/dynamics/periodic_pts.lean Outdated Show resolved Hide resolved
src/dynamics/periodic_pts.lean Show resolved Hide resolved
src/dynamics/periodic_pts.lean Outdated
@@ -368,4 +412,62 @@ lemma minimal_period_iterate_eq_div_gcd' (h : x ∈ periodic_pts f) :
minimal_period_iterate_eq_div_gcd_aux $
gcd_pos_of_pos_left n (minimal_period_pos_iff_mem_periodic_pts.mpr h)

/-- The orbit of a periodic point `x` of `f` is the cycle `[x, f x, f (f x), ...]`. Its length is
the minimal period of `x`. -/
def orbit (f : α → α) (x : α) : cycle α :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

I have two concerns about this definition:

  1. Doesn't this mean that the orbit of a non-periodic point is empty? I don't think this is usually what one means by orbit.
  2. Why is this of type cycle α and not just set α?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

  1. Yes, as this is the only reasonable output given the output type.

  2. Orbits have a very nice cyclic structure and I believe that should be reflected in the output type. After all, it's very easy to retrieve a list or a set from the definition I'm using, while doing the opposite is quite harder.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Another reason this definition is nice is that it plays very well with cycle.pairwise. One can deduce properties about the entire orbit just by proving them for x and f x.

Copy link
Collaborator

Choose a reason for hiding this comment

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

One can deduce properties about the entire orbit just by proving them for x and f x.

On the other hand, using cycle means we can only do this when the orbit is finite which is a big restriction.

I agree that it is useful to be able to talk about orbits of functions so this is a sensible definition to make (albeit probably in a different file). Indeed this should probably be used to generalise https://leanprover-community.github.io/mathlib_docs/group_theory/group_action/basic.html#mul_action.orbit

I also agree that the induction principle you mention (sufficient to prove for x and f x) is worth having but I'm afraid I'm still not convinced that we should use cycle to obtain this.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

You're right that the induction principle I mentioned doesn't really need this construction. That said, I still believe that this particular construction is useful, or at the very least of mathematical interest. One particular example I can recall is the study of finite symmetric groups.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

In fact, I've started work on a PR to add a few lemmas about these orbits to group_theory.perm.cycles. I think it should be much clearer why this is the correct definition for that specific use case.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I agree with @ocfnash that this shouldn't be called orbit, as orbit f x must mean the set of iterated images of x under f.

Perhaps periodic_orbit?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Sure, periodic_orbit it is.

@ocfnash ocfnash 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 Apr 13, 2022
vihdzp and others added 2 commits April 13, 2022 20:43
@vihdzp @ocfnash
Update src/dynamics/periodic_pts.lean
3cd2e0a 
Co-authored-by: Oliver Nash <github@olivernash.org>
@vihdzp @ocfnash
Update src/dynamics/periodic_pts.lean
b89c5f0 
Co-authored-by: Oliver Nash <github@olivernash.org>
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 26, 2022
@vihdzp vihdzp 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 May 7, 2022
@vihdzp @urkud
Update src/dynamics/periodic_pts.lean
fd85dfd 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@semorrison semorrison 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 May 17, 2022
@vihdzp vihdzp 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 May 20, 2022
@fpvandoorn fpvandoorn requested a review from ocfnash June 4, 2022 12:00
ocfnash
ocfnash approved these changes Jun 9, 2022
View reviewed changes
Copy link
Collaborator

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

I still have reservations about using cycle instead of set but I seem to be alone in this opinion so let's try this out and see how we go.

Please apply my suggestions and then feel free to merge.

bors d+

src/dynamics/periodic_pts.lean Outdated Show resolved Hide resolved
src/dynamics/periodic_pts.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Jun 9, 2022

✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jun 9, 2022
@vihdzp vihdzp added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 10, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 10, 2022
@vihdzp
Copy link
Collaborator Author

vihdzp commented Jun 10, 2022

bors r+

bors bot pushed a commit that referenced this pull request Jun 10, 2022
@vihdzp
feat(dynamics/periodic_pts): Orbit under periodic function (#12976)
39184f4
@bors
Copy link

bors bot commented Jun 10, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(dynamics/periodic_pts): Orbit under periodic function [Merged by Bors] - feat(dynamics/periodic_pts): Orbit under periodic function Jun 10, 2022
@bors bors bot closed this Jun 10, 2022
@bors bors bot deleted the orbit_pp branch June 10, 2022 10:04
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

@semorrison semorrison semorrison left review comments

@ocfnash ocfnash ocfnash approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@vihdzp @leanprover-community-bot-assistant @urkud @semorrison @ocfnash