Trigonometric functions

Stream: new members

[Sebastian Zimmer]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastian Zimmer]

Is that available in a public repo somewhere?

[Chris Hughes]

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

[Sebastian Zimmer]

awesome thanks

[Sebastian Zimmer]

It's surprising how much you can prove without calculus

[Johan Commelin]

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

[Chris Hughes]

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

[Chris Hughes]

After that I'll PR it.

[Sebastian Zimmer]

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.

[Chris Hughes]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Sebastian Zimmer]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

which is stronger

[Kevin Buzzard]

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

[Sebastian Zimmer]

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

[Sebastian Zimmer]

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

[Chris Hughes]

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 $x \le 1$

[Kevin Buzzard]

yes exactly. So e.g. for $0\le x \le4$ maybe you only know that $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.

[Chris Hughes]

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

[Sebastian Zimmer]

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

[Sebastian Zimmer]

Probably would be easy from what you have already done

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Chris Hughes]

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.

[Mario Carneiro]

Do you have complex log?

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I'll have you know mathematicians invented branch cuts

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe I just don't like the definitions.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

0^0 is another example

[Mario Carneiro]

partial functions are possible but a bad idea in dtt

[Kevin Buzzard]

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".

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Kevin Buzzard]

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 $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.

[Reid Barton]

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

[Patrick Massot]

Indeed it would be nice to have FTA

[Kevin Buzzard]

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.

[Reid Barton]

metamath uses this proof as far as I can tell

[Reid Barton]

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

[Patrick Massot]

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)

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

wait, which thread am I on

[Mario Carneiro]

it also has contour integrals

[Mario Carneiro]

which we don't have

[Kenny Lau]

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

[Kenny Lau]

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

[Chris Hughes]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

Chris is writing a calculator emulator.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

Finally, someone having common sense!

[Patrick Massot]

Now stop kidding: where is our sheaf theory?

[Kevin Buzzard]

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

[Chris Hughes]

@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.

[Kevin Buzzard]

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

[Patrick Massot]

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

[David Michael Roberts]

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

[Mario Carneiro]

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

more like the entire theory of analytic functions

[Kevin Buzzard]

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.

[Patrick Massot]

I never heard of those characterizations before following the link yesterday

[Bryan Gin-ge Chen]

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.

[Kevin Buzzard]

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

[Chris Hughes]

(deleted)

[Antoine Chambert-Loir]

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.

[Kevin Buzzard]

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