Trig function values

Stream: general

[Heather Macbeth]

An undergraduate student of mine, @Benjamin Davidson , has written up some missing trig function values -- $\cos(\pi/4)$ and similar. He has bigger plans, but to me, this already seems like a reasonable first PR. What do others think?

[Shing Tak Lam]

I don't know what they already have, or if this is useful, but here are a few lemmas to do with cos and sin that I've proven a few weeks ago. Might be worth bundling into one PR? Or should I PR these separately?

https://gist.github.com/shingtaklam1324/4cd8a22113e0c3db0219b7751336fdd3

[Heather Macbeth]

I think PRs can be arbitrarily small, so no need to combine them. But to me, this definitely also looks worth PR'ing.

[Johan Commelin]

Yup, especially a first PR shouldn't try to be big.

[Johan Commelin]

PR's are cheap.

[Kevin Buzzard]

If it's of any interest, I remember when I was at school knowing sin(15)=(sqrt(6)-sqrt(2))/4 and sin(18)=(sqrt(5)-1)/4.

[Kevin Buzzard]

And I think that when I was at uni I convinced myself that things wouldn't go much further, in the sense that you start needing square roots of square roots after that.

[Floris van Doorn]

cos(pi / 4) and similar values already exists in mathlib:
https://github.com/leanprover-community/mathlib/blob/master/src/data/real/pi.lean#L101
I think this file was forgotten when properties about trigonometric functions were refactored into this file:
https://github.com/leanprover-community/mathlib/blob/master/src/analysis/special_functions/trigonometric.lean

[Heather Macbeth]

@Floris van Doorn , thanks for linking. In my opinion, the first half of that file (everything with a sin or cos in the name) should be refactored into analysis.special_functions.trigonometric

[Heather Macbeth]

And the rest (the facts purely about $\pi$) left in data.real.pi. What do you think?

[Floris van Doorn]

I agree. I think everything until line 123 should go into special_functions.trigonometric: it's more about trig than about pi.

[Heather Macbeth]

That sounds great. Maybe @Benjamin Davidson can do this reorganization. He also proved a few facts that are not in your file (for example, $\tan(\pi/4)$ and $\tan^{-1}(1)$), which he could add.

[Joseph Myers]

Wikipedia has a very long list of such values, but maybe they wouldn't all be appropriate for mathlib (that page has a warning they might not all be appropriate for Wikipedia either). DLMF has a shorter table for multiples of $\pi/12$; maybe multiples of $\pi/8$, $\pi/10$ and $\pi/12$ cover most of the cases likely to be useful in practice (along with $\pi/17$ and $2\pi/17$ as a well-known result even if not one anything else is likely to use).

[Jalex Stark]

Getting the whole list may be a nice exercise in automation :)

[Kevin Buzzard]

or more homework for @Benjamin Davidson :-)

[Jalex Stark]

right, I suppose "automation" could also just mean "proving helper lemmas" rather than "writing tactics"

[Kevin Buzzard]

So for me, square roots of square roots was too much (I could see you could go on forever this way), but I didn't know $\tan(7.5^\degree)=\sqrt{6}-\sqrt{3}+\sqrt{2}-2$.

[Jalex Stark]

that's a pretty number

[Kevin Buzzard]

I remember one thing bothering me when I was at school -- there are nice "no square roots of square roots" formulas for both $\sin(15)$ and $\cos(15)$, but even though $\sin(18)$ came out nicely, I couldn't figure out how to get $\cos(18)$ without taking a square root of a square root. I guess nowadays I can prove it's impossible :-)

[Kevin Buzzard]

Thanks for the link Joseph, that Wikipedia page is a work of art.

[Benjamin Davidson]

Hi all, I'm Ben and I am more than happy to PR anything deemed useful! May I please have GitHub access so that I can work on making my first PR?

[Benjamin Davidson]

@Floris van Doorn Thank you for sharing this file, I hadn't come across it and had only checked analysis.special_functions.trigonometric for the likes of cos (pi/4).

[Jalex Stark]

Benjamin Davidson said:

Hi all, I'm Ben and I am more than happy to PR anything deemed useful! May I please have GitHub access so that I can work on making my first PR?

what's your github username?

[Floris van Doorn]

Benjamin Davidson said:

Floris van Doorn Thank you for sharing this file, I hadn't come across it and had only checked analysis.special_functions.trigonometric for the likes of cos (pi/4).

Makes sense. They are in an unexpected place.

[Benjamin Davidson]

@Jalex Stark My GitHub username is benjamindavidson

[Scott Morrison]

@Benjamin Davidson: See https://github.com/leanprover-community/mathlib/invitations

[Benjamin Davidson]

@Scott Morrison Thank you

[Benjamin Davidson]

#3497