Zulip Chat Archive

Stream: new members

Topic: Trigonometric functions


view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 13:34):

I'd like to learn how to use lean, by attempting to prove something nontrivial. Looking through the potential projects wiki page, trigonometric functions seems like the most promising (in that I can confidently prove the basic identies, facts about pi, etc. from first principles).

I don't have much experience with theorem provers (I've used idris and coq in the past, but not terribly successfully).

The wiki links to some progress on the exponential function https://github.com/leanprover/mathlib/pull/41/commits/6b1f85b149329be0c9084081668230c2d622f387
but I can't tell if anything came of that.

  • Does this seem feasible?
  • What is the state of power series / exponential functions / trigonometric functions in mathlib?
  • What would I build on top of? Are there other things in development that would be helpful to me?

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 13:36):

There was a whole bunch of stuff formalised recently. I think we got exp, log, pi, sin, cos, tan

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 13:37):

and double angle formulae etc. All of this is about a week old

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 13:37):

Apparently we have cos(pi/2)=0 but we can only deduce that sin(pi/2)=+-1 ;-)

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 13:46):

Is that available in a public repo somewhere?

view this post on Zulip Chris Hughes (Sep 29 2018 at 13:49):

https://github.com/leanprover-community/mathlib/tree/exp

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 13:50):

awesome thanks

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 14:10):

It's surprising how much you can prove without calculus

view this post on Zulip Johan Commelin (Sep 29 2018 at 14:24):

@Chris Hughes When will you PR exp? Is there some list of things you still want to add to it?

view this post on Zulip Chris Hughes (Sep 29 2018 at 14:25):

I still need sin(p/2)=1, and the inverses of all 14 functions

view this post on Zulip Chris Hughes (Sep 29 2018 at 14:25):

After that I'll PR it.

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 16:03):

Just out of interest @Chris Hughes , how are you planning on proving sin(pi / 2) > 0? I can't see a way of doing it without a bit of calculus.

view this post on Zulip Chris Hughes (Sep 29 2018 at 16:08):

I think I should be able to prove some bounds on it in a similar way to the bounds on cos. @Mario Carneiro told me the method
sin (2*x) is positive for all 0<x<=1 because sin x and cos x are
x - x^3/3 < sin x < x and 1 - 2/3 * x^2 < cos x < 1 - x^2/3 on (0, 1] by infinite series bounds

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 16:17):

Chris I mentioned the general result from which this follows to you the other day. If you have a sequence a1,a2,a3,... with the signs of the terms alternating, and the terms tending to zero, then not only does the sum of the sequence converge, but the sum is <= all the odd partial sums (if a1>0) and >= all the even ones.

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 16:18):

This is a fabulous tool for getting bounds for anything. You don't even need 0<x<=1, it will work for any real x because after sufficiently many terms they will start alternating in sign and decreasing

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 16:19):

that gives you x - x^3/3 < sin(x) but I don't see why 1 - 2/3 x^2 < cos(x)

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 16:20):

1-x^2/2<cos(x) for 0<x<1 by this result

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 16:20):

which is stronger

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 16:22):

these tricks tell you that the partial sums are good approximations to sin and cos for x small, and because you know where the roots are you can start proving goofy things like sum 1/n^2 = pi^2/6 like this, but the details are messy

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 16:23):

Can we show that e.g. sin has only one root close to \pi without calculus?

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 16:24):

actually I can see how to do it using some identities that are already proven

view this post on Zulip Chris Hughes (Sep 30 2018 at 08:43):

Chris I mentioned the general result from which this follows to you the other day. If you have a sequence a1,a2,a3,... with the signs of the terms alternating, and the terms tending to zero, then not only does the sum of the sequence converge, but the sum is <= all the odd partial sums (if a1>0) and >= all the even ones.

But it's only less than the partial sums after the sequence starts decreasing right. Which complicates proofs a lot without x1x \le 1

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 09:01):

yes exactly. So e.g. for 0x40\le x \le4 maybe you only know that xx33!sin(x)xx33!+x55!x-\frac{x^3}{3!} \le \sin(x)\le x-\frac{x^3}{3!}+\frac{x^5}{5!}. But if people want to know things like cos(pi) then this approach will work.

view this post on Zulip Chris Hughes (Sep 30 2018 at 20:02):

I now have sin(x)>0\sin(x)>0 for 0<x<π0<x<\pi, and therefore sin(π2)=1\sin\left(\frac{\pi}{2}\right)=1

view this post on Zulip Sebastian Zimmer (Sep 30 2018 at 20:05):

Are you going to do sin(x)=0x=kπ\sin(x) = 0 \iff x = k * \pi?

view this post on Zulip Sebastian Zimmer (Sep 30 2018 at 20:06):

Probably would be easy from what you have already done

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 20:47):

One can probably prove that if sin (t)=0 then sin (x+2t)=sin(x) I guess? And the periods of a function are a subgroup of the reals so there's a pure thought approach to the result -- pi is in and no positive real less than pi, so it's the multiples of pi

view this post on Zulip Patrick Massot (Sep 30 2018 at 20:48):

I don't thing mathlib has the classification of subgroups of reals

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 20:49):

This one isn't hard though, write any x in the group as n*pi +r with 0<=r<pi and then sin(r)=0 so by Chris's result r=0

view this post on Zulip Mario Carneiro (Sep 30 2018 at 21:12):

yes, this is basically how I sketched the proof that 2<pi < 4 with the alternate definition of pi as the least positive zero of sin. The addition formula of sin shows that zeros of sin are closed under Z module operations

view this post on Zulip Chris Hughes (Oct 01 2018 at 17:25):

Today I did arctan, arcsin and arccos, for reals, and proved that they are two-sided inverses within the appropriate intervals. Not sure how to do the same for complexes.

view this post on Zulip Mario Carneiro (Oct 01 2018 at 17:26):

Do you have complex log?

view this post on Zulip Mario Carneiro (Oct 01 2018 at 17:27):

How far in https://leanprover.zulipchat.com/#narrow/stream/141825-kbb/subject/sine.20and.20cosine.20and.20pi/near/134258931 have you got?

view this post on Zulip Chris Hughes (Oct 01 2018 at 17:46):

complex.log is my next target. I think that can just be done with real.log and real.arctan

view this post on Zulip Mario Carneiro (Oct 01 2018 at 17:49):

hm, I guess you are right... I didn't have inverse trig when I did log

view this post on Zulip Mario Carneiro (Oct 01 2018 at 17:50):

still, you want the injectivity statement anyway (exp z = 0 <-> z/2 pi i is an integer)

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:34):

Wait -- what is complex.log? It'll be discontinuous, right? log is multi-valued (except at zero, where it's 37).

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:37):

Geometrically, the map exp from the complexes to themselves is an infinite sheeted unramified cover from the complex numbers to the non-zero complex numbers. Unramified means that given any non-zero complex number in the target, you can draw a tiny disc around it and the pre-image of that tiny disc in the source is lots of copies of the tiny disc (in this case countably infinitely many, and a Z-torsor). What information does a presumably non-computable log give you about this picture? Isn't the correct definition of "log" just literally the subset of the complexes whose exp is the thing you're trying to take the log of? complex.log is ugly. Is it actually used in pure mathematics?

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:38):

It could map to the product of the reals and R/2πZ\mathbb{R}/2\pi\mathbb{Z}

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:39):

log(reiθ)=(log(r),θ)\log(re^{i\theta})=(\log(r),\theta).

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:42):

complex.log is ugly. Is it actually used in pure mathematics?

Yes, absolutely yes. Trying to make sense of "multivalued functions" is a hundred times harder than just picking a branch cut and being consistent about it

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:45):

My proposed mangling of this function: log x is the unique value with exp (log x) = x and -pi < Im (log x) <= pi, with log 0 = 0

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:46):

You guys think about maths in such an ugly way. I painted a beautiful picture and you just rip a branch out of it.

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:46):

I'll have you know mathematicians invented branch cuts

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:47):

And yet actually Lean taught me a much more beautiful proof of the Hilbert Basis Theorem.

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:47):

Maybe I just don't like the definitions.

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 22:47):

I've been grumpy about 1/0 since day 1.

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:55):

I don't understand why mathematicians have such a hard time coming to grips with the fact that not all functions are continuous

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:57):

and when faced with evidence to the contrary they assume that points of discontinuity aren't in the domain

view this post on Zulip Simon Hudon (Oct 01 2018 at 22:57):

I've been grumpy about 1/0 since day 1.

I'm not too fond of that either. PVS has a nice answer to that, you always have to prove that the denominator is \ne 0. I'm wondering if we could do that nicely with notation like this:

notation x ` / ` y := div' x y (by assumption)

This way, x / y would only be type correct if one of your assumption is y ≠ 0

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:58):

0^0 is another example

view this post on Zulip Mario Carneiro (Oct 01 2018 at 22:59):

partial functions are possible but a bad idea in dtt

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 23:19):

I'm hapoy not to open this can of worms again. My point is simply that it is still a surprise to me that CS guys think about mathematics in different ways to mathematicians. I really do not ever run into discontinuous functions in my work, and if you think I do (given that I run into division but am careful never to divide by zero) then in some sense I regard this as evidence that you're thinking about it wrongly, but conversely I think Mario's point is far more relevant in this context than what I think beautiful maths looks like. We are thinking about the same things but in some sense the mathematician seems to carry around some extra nuance, or perhaps some unwritten instructions on how to use the function properly and how to avoid the sharp edges. "Warning -- if you're dividing by zero you're probably doing it wrong".

view this post on Zulip Mario Carneiro (Oct 01 2018 at 23:26):

I think that's fair. Essentially, myself and other logicians / computer scientists are calling the mathematicians out when they talk about functions that don't meet the chapter 1 definition

view this post on Zulip Mario Carneiro (Oct 01 2018 at 23:27):

mathematical aesthetics decrees that everything interesting is continuous, and so this causes some cognitive dissonance in the mind of the mathematician that requires some additional equivocation on these setups when pressed

view this post on Zulip Mario Carneiro (Oct 01 2018 at 23:28):

but as soon as you stop pressing they go back to treating log\log like a plain function

view this post on Zulip Mario Carneiro (Oct 01 2018 at 23:30):

I think that there absolutely are other construals of this function as a Riemann surface or smooth manifold, but when it gets down to plain calculation you want to be able to pick a locally coherent section of the function and know what's going on there

view this post on Zulip Mario Carneiro (Oct 01 2018 at 23:32):

Note that from this "principal log", you can still have your manifold by rotating the reference frame so that your point of interest is on the real line

view this post on Zulip Patrick Massot (Oct 02 2018 at 07:01):

Is there any point in pushing this low-tech trigonometry further? I agree that having pi, and real trigonometry functions is nice for teaching. But who will teach complex logarithm without the basics of holomorphic functions? If someone does Cauchy theory then we can properly state that holomorphic functions have primitive on simply connected open subsets of their domain of definition. Then1/z will have a primitive function on any simply connected open set not containing zero, and we'll be able to easily relate those primitive to exponential.

view this post on Zulip Patrick Massot (Oct 02 2018 at 07:02):

Of course we could also do Riemann surfaces if someone prioritizes this, but I don't see happening soon

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 07:10):

My personal stance on this is very clear: there is an essentially random amount of this stuff which I personally wanted to see in Lean, which is the stuff which shows up in my elementary course. For example eiθ=cos(θ)+isin(θ)e^{i\theta}=\cos(\theta)+i\sin(\theta). But now we have all of this, because Chris took my course last year and has now covered everything, so I am no longer pushing for any more of this stuff. I just needed enough to be able to formalise the questions I ask the students. Maybe in the future we will need more but I am not pressing for any of it right now -- I feel that we have enough to look respectable to mathematicians.

view this post on Zulip Reid Barton (Oct 02 2018 at 10:57):

One of the standard proofs of the fundamental theorem of algebra requires as input the fact that zn=az^n = a has a root for any complex aa, which needs about this level of trig. Or to prove te2πitt \mapsto e^{2\pi i t} is a local homeomorphism from R\mathbb{R} to the unit circle is similar (which also implies FTA via covering space theory).

view this post on Zulip Patrick Massot (Oct 02 2018 at 10:58):

Indeed it would be nice to have FTA

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 11:03):

This is one of those theorems for which there are about 20 proofs, isn't it. Before embarking on one in Lean I guess it's important to see how it is proved in other provers and what other options there are. The proof I saw used complex analysis and integration around a big circle if I remember correctly. But maybe I saw some completely different one years later which went via a real-analytic proof that every polynomial over the reals factored into terms of degree at most 2.

view this post on Zulip Reid Barton (Oct 02 2018 at 11:09):

metamath uses this proof as far as I can tell

view this post on Zulip Reid Barton (Oct 02 2018 at 11:11):

I know this because someone on my Twitch stream mentioned that they were trying to prove FTA in Lean, working from the metamath proof. Kevin I am guessing it is a student of yours based but I'm not sure

view this post on Zulip Patrick Massot (Oct 02 2018 at 11:15):

I saw dozens of proofs of this theorem. Of course all the nice ones are more or less openly based on elementary algebraic topology. But I also saw a proof using only algebra and existence of roots for odd degree real polynomials (easy consequence of limits and intermediate value theorem)

view this post on Zulip Mario Carneiro (Oct 02 2018 at 17:01):

The metamath proof of FTA is my favorite (of course, I wrote it!). It is based on this wikipedia proof. The main topological prerequisite is the extreme value theorem: A large closed ball about zero in C is compact, so abs (p z) takes a minimum value somewhere. The rest is just reasoning about finite sums

view this post on Zulip Kenny Lau (Oct 02 2018 at 17:03):

I've seen a short proof using a clever contour integral

view this post on Zulip Kenny Lau (Oct 02 2018 at 17:04):

but I recall it has cosine so maybe it isn't suitable

view this post on Zulip Kenny Lau (Oct 02 2018 at 17:04):

wait, which thread am I on

view this post on Zulip Mario Carneiro (Oct 02 2018 at 17:04):

it also has contour integrals

view this post on Zulip Mario Carneiro (Oct 02 2018 at 17:04):

which we don't have

view this post on Zulip Kenny Lau (Oct 02 2018 at 17:04):

yes, I mean the proof I saw uses one contour integral

view this post on Zulip Kenny Lau (Oct 02 2018 at 17:05):

actually I think the proof from Galois theory may have some potential

view this post on Zulip Chris Hughes (Oct 03 2018 at 19:17):

PRed https://github.com/leanprover/mathlib/pull/386. I stopped at complex log. No inverse complex trig yet. Not sure whether a highbrow method is better for that.

view this post on Zulip Mario Carneiro (Oct 03 2018 at 19:58):

The metamath definitions
arcsinz=ilog(iz+(1z2)1/2)\arcsin z = -i\log(iz + (1-z^2)^{1/2})
arccosz=π/2arcsinz\arccos z = \pi/2-\arcsin z
arctanz=i2[log(1iz)log(1+iz)]\arctan z = \frac i2\left[\log(1-iz) - \log(1 + iz)\right]
make sure to put the branch cuts in the right places

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 20:00):

Chris is writing a calculator emulator.

view this post on Zulip Mario Carneiro (Oct 03 2018 at 20:00):

(I don't see a sqrt in the first expression where the conspicuous space is, but pretend there is one)

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 20:04):

I've been fixing that on this forum by using ^{1/2}. \sqrt never works for me.

view this post on Zulip Reid Barton (Oct 03 2018 at 20:05):

Do we have enough now to show that every complex number can be written in the form reiθre^{i \theta}?

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 20:07):

This might boil down to showing that if x2+y2=1x^2+y^2=1 then there exists θ\theta such that x=cos(θ)x=\cos(\theta) and y=sin(θ)y=\sin(\theta). If only we'd defined sin\sin as opposite over hypotenuse :-)

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:09):

If only we'd defined sin\sin as opposite over hypotenuse :-)

Finally, someone having common sense!

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:10):

Now stop kidding: where is our sheaf theory?

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 20:11):

Hey, maybe atan(y/x)atan(y/x) (possibly plus π\pi) can be proved to work.

view this post on Zulip Chris Hughes (Oct 03 2018 at 20:11):

@Reid Barton I didn't prove that directly, but we have arg and cos (arg x) = x.re / abs x and similar for sin, so it should be easy.

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 20:20):

If we prove the product rule then mathlib might be able to pass A-level! (UK maths exam for 18 year olds)

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:21):

We sort of have it in the holomorphic case https://github.com/semorrison/kbb/blob/master/src/holomorphic_functions.lean#L117

view this post on Zulip David Michael Roberts (Oct 03 2018 at 23:47):

It's surprising how much you can prove without calculus

it might be worth formalising some of this, if possible: https://ncatlab.org/toddtrimble/published/Characterization+of+sine

view this post on Zulip Mario Carneiro (Oct 03 2018 at 23:56):

and we get to invoke the theory of entire analytic functions.

more like the entire theory of analytic functions

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 06:47):

I never quite know whether it's worth formalising "gimmicks". I mean, I've taught this stuff, and never once have I used or seen the use of this linked result -- the characterisation. It's very cute for sure. But does it deserve to be in mathlib? I genuinely don't know.

view this post on Zulip Patrick Massot (Oct 04 2018 at 06:52):

I never heard of those characterizations before following the link yesterday

view this post on Zulip Bryan Gin-ge Chen (Oct 04 2018 at 06:55):

Presumably there are many math results worth formalizing that don't deserve to be in mathlib. I think a well-documented formalization of the above characterization of sine could potentially make a fun tutorial to the new functions that Chris is PRing.

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 09:01):

I think that this is a really good way of looking at it.

view this post on Zulip Chris Hughes (Oct 27 2018 at 09:19):

(deleted)

view this post on Zulip Antoine Chambert-Loir (Sep 29 2019 at 22:45):

The proof you mention has the virtue of being valid for all real closed fields.
There is also a very nice proof by Kneser (1981) (and Kneser 1940) inspired by the classical proof that considers the minimum value of a polynomial and, if non zero, finds an even smaller value. But his proof is even intuitionistically valid: it gives an algorithm that converges to a root with known speed.

view this post on Zulip Kevin Buzzard (Sep 29 2019 at 23:03):

Since this thread (1 year old) Chris formalised FTA and it's now in mathlib


Last updated: May 11 2021 at 12:15 UTC