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/special_functions/trigonometric): range_{exp,cos,sin} #4595

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} #4595

wants to merge 10 commits into from

Conversation

jcommelin
Copy link
Member

@jcommelin jcommelin commented Oct 13, 2020 •
edited by github-actions bot

@jcommelin jcommelin added the awaiting-review The author would like community review of the PR label Oct 13, 2020
@jcommelin jcommelin changed the title feat(analysis/special_functions/trigonometric): range_cos_infinite feat(analysis/special_functions/trigonometric): range_{cos,sin}_infinite Oct 13, 2020
@jcommelin jcommelin mentioned this pull request Oct 14, 2020
Closed
5 tasks
@hrmacbeth
Copy link
Member

Is there a generalization lurking here? Is it true that a path-connected Hausdorff space is either a singleton or infinite, or something along these lines? @urkud

@bryangingechen
Copy link
Collaborator

Is there a generalization lurking here? Is it true that a path-connected Hausdorff space is either a singleton or infinite, or something along these lines? @urkud

I just found this: https://topospaces.subwiki.org/wiki/Path-connected_and_T1_with_at_least_two_points_implies_uncountable

@hrmacbeth
Copy link
Member

Great! And yes, I think one can do (fairly quickly?) finite + Hausdorff -> discrete; connected + discrete -> singleton. @jcommelin, do you have the energy for this generalization? I can share the work if you like.

@hrmacbeth
Copy link
Member

On second thoughts ... the connectedness of the range would probably be established from its being literally an interval (real.range_cos), at which point it's silly to get the infinitude from Hausdorffness when you already have a single-lemma proof of the infinitude from your orders lemma (Icc.infinite). So I think my idea

finite + Hausdorff -> discrete; connected + discrete -> singleton

is less efficient (even modulo a pre-existing perfect library) than your current version. What do you think?

bors d+

@bors
Copy link

bors bot commented Oct 16, 2020

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

@jcommelin
Copy link
Member Author

I guess you can also get connectedness of the range from continuity and connectedness of the domain, so with a perfect library the proof might become a little bit shorter. But I won't have time to work on that in the near future.

@jcommelin jcommelin changed the title feat(analysis/special_functions/trigonometric): range_{cos,sin}_infinite feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} Oct 17, 2020
@jcommelin jcommelin 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 17, 2020
@jcommelin
Copy link
Member Author

@hrmacbeth @urkud this PR changed a lot, so I don't think it's fair if I (ab)use the bors d+ to merge this PR myself. Could one of you take another look please?

@hrmacbeth
Copy link
Member

@jcommelin does #4656 need to be merged first? Who is the canonical reviewer for that?

@jcommelin
Copy link
Member Author

I think anybody can review that. It's mostly cleaning up... weakening assumptions, using readable names for variables, moving things to the proper location.

urkud
urkud reviewed Oct 17, 2020
View reviewed changes
src/analysis/special_functions/trigonometric.lean
@@ -1658,6 +1669,21 @@ lemma log_I : log I = π / 2 * I := by simp [log]

lemma log_neg_I : log (-I) = -(π / 2) * I := by simp [log]

lemma exists_pow_nat_eq (x : ℂ) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x :=
Copy link
Member

@urkud urkud Oct 17, 2020 •
edited

Choose a reason for hiding this comment

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

TODO (not necessarily for this PR): generalize these two lemmas to an [is_alg_closed] field and add an instance [is_alg_closed complex].

Copy link
Collaborator

Choose a reason for hiding this comment

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

It would be a good idea to create an issue if you won't be working on it immediately.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Maybe I'm misunderstanding the comment, but we did have the complex.is_alg_closed instance:

mathlib/src/field_theory/algebraic_closure.lean

Line 72 in 09afb04

instance complex.is_alg_closed : is_alg_closed ℂ :=

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 17, 2020
@bryangingechen bryangingechen 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 18, 2020
@PatrickMassot
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 18, 2020
@bors
Copy link

bors bot commented Oct 18, 2020

Merge conflict.

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 18, 2020
@PatrickMassot
Copy link
Member

bors merge

bors bot pushed a commit that referenced this pull request Oct 18, 2020
@jcommelin @PatrickMassot
feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} (#…
93b7e63 
…4595)

Co-authored-by: Patrick Massot <patrickmassot@free.fr>
@bors
Copy link

bors bot commented Oct 18, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} [Merged by Bors] - feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} Oct 18, 2020
@bors bors bot closed this Oct 18, 2020
@bors bors bot deleted the chebpoly-preps-3 branch October 18, 2020 21:34
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

@ADedecker ADedecker ADedecker 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
6 participants
@jcommelin @hrmacbeth @bryangingechen @PatrickMassot @urkud @ADedecker