## Stream: kbb

### Topic: hello

Welcome to #kbb.

#### Patrick Massot (Sep 11 2018 at 20:28):

This is a test: can anyone hear me?

Yes

#### Patrick Massot (Sep 11 2018 at 20:28):

Does anyone has another Zulip account and could check what is visible?

#### Reid Barton (Sep 11 2018 at 20:28):

I thought about this, but I'm not sure whether the stream would be visible to external people. Yeah

#### Reid Barton (Sep 11 2018 at 20:29):

Or, just remove me temporarily.

#### Patrick Massot (Sep 11 2018 at 20:29):

Funnily, I don't seem to be allowed to do that

I see you

#### Patrick Massot (Sep 11 2018 at 20:32):

I'm creating another account

#### Simon Hudon (Sep 11 2018 at 20:32):

Also: this is a great idea

#### Simon Hudon (Sep 11 2018 at 20:33):

Did you need the help of an administrator to create this stream?

No

#### Patrick Massot (Sep 11 2018 at 20:34):

I think this stream is safe

#### Patrick Massot (Sep 11 2018 at 20:34):

The point is that group PM is not suitable for what we were doing. That generates too many notifications

Amen

#### Patrick Massot (Sep 11 2018 at 20:36):

Reid, do you see things here?

#### Patrick Massot (Sep 11 2018 at 20:37):

Reid should be back in

Yep, I am now.

#### Patrick Massot (Sep 11 2018 at 20:38):

And should see the full history, which is another advantage compared to group PM

Indeed I can

#### Patrick Massot (Sep 11 2018 at 20:38):

(this was an option when creating the stream)

#### Patrick Massot (Sep 11 2018 at 20:39):

Ok, let's stop using the group PM and its endless series of emails and notification popups

#### Patrick Massot (Sep 11 2018 at 20:39):

Did you need the help of an administrator to create this stream?

No

#### Patrick Massot (Sep 11 2018 at 20:41):

What's the story of fast_matrix? Is it fast to compute because it uses vector? Or is it only fast to type because of the notation?

#### Johan Commelin (Sep 12 2018 at 02:22):

What's the story of fast_matrix? Is it fast to compute because it uses vector? Or is it only fast to type because of the notation?

Shouldn't this go into a new thread :rolling_on_the_floor_laughing:

#### Johan Commelin (Sep 12 2018 at 02:24):

To answer your question: fast_matrix is now obsolete, since @Jack Crawford pushed an implementation that is a lot more fleshed out. His implementation is both supposed to be faster to compute with and easier to type. You can use the equation compiler to grab the a b c d out of a 2x2 matrix, which makes for readable definitions.

#### Johan Commelin (Sep 12 2018 at 02:25):

Also: very good idea to create a private stream. I didn't know this was possible. We should have done that 1 week ago.

#### Johan Commelin (Sep 12 2018 at 02:26):

The cool side effect is that we can give Kevin access, and he can read through the history of all of our discussions :lol:

#### Kenny Lau (Sep 16 2018 at 08:48):

ok so we have 4 days left

#### Kenny Lau (Sep 16 2018 at 08:48):

can we come up with a realistic list of goals

#### Kenny Lau (Sep 16 2018 at 08:48):

or a list of realistic goals?

#### Patrick Massot (Sep 16 2018 at 16:08):

Mario, do you see anything in this repo that could hope to get into mathlib?

#### Johan Commelin (Sep 17 2018 at 04:03):

Like I said, I'll be gone on Wednesday, so I can only contribute today and tomorrow.

#### Johan Commelin (Sep 17 2018 at 04:04):

I think either: we start cleaning up; or we focus on the Hecke operator (on the complex vector space (=module :lol:) of modular forms.

#### Johan Commelin (Sep 17 2018 at 04:04):

This second option will probably force us to clean up other stuff as well.

#### Johan Commelin (Sep 17 2018 at 04:05):

Otoh, we could also leave the modular form part of the repo as it is.

#### Johan Commelin (Sep 17 2018 at 04:05):

And then we could focus all our time on exp and friends.

#### Johan Commelin (Sep 18 2018 at 06:41):

:bell: We have 99 commits in the kbb repository! Well done to everyone who contributed!

#### Patrick Massot (Sep 18 2018 at 08:52):

What's the status of the Hecke operator file? I don't even understand the maths here. What is the meaning of the first displayed formula at https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula? Is each term in the sum meant to be well defined? Or only the sum? If I naively try to change (a b c d) by multiplication by a element of SL2Z and use the weight formula for f, I don't seem to get the same term.

#### Johan Commelin (Sep 18 2018 at 09:04):

You should get the same term, right? Or did I mess something up. I was quite convinced that every term in the sum was well-defined.

#### Johan Commelin (Sep 18 2018 at 09:05):

But maybe we should just delete this file... I think I aimed to high.

#### Patrick Massot (Sep 18 2018 at 09:06):

I don't understand the wikipedia page, so you don't need to mess up anything

#### Patrick Massot (Sep 18 2018 at 09:06):

What is the pen and paper proof that each term in the sum is well-defined?

#### Patrick Massot (Sep 18 2018 at 09:07):

I must be missing something obvious

#### Johan Commelin (Sep 18 2018 at 09:08):

$(cz + d)^{-k} f(\frac{az + b}{cz + d}) = (cz + d)^{-k} f(\begin{pmatrix} a & b \\ c & d \end{pmatrix}z)$, is that right?

yes

#### Johan Commelin (Sep 18 2018 at 09:08):

So now we take another representative: $M\begin{pmatrix}a & b \\ c & d \end{pmatrix}$

#### Patrick Massot (Sep 18 2018 at 09:09):

The trouble is that $a, b, c, d \mapsto (cz+d)$ is not a group morphism

#### Johan Commelin (Sep 18 2018 at 09:10):

Hmm, I'm also getting myself confused.

#### Patrick Massot (Sep 18 2018 at 09:11):

If that were a group morphism then everything would be obviously ok

#### Reid Barton (Sep 18 2018 at 09:13):

It shouldn't be a group morphism, it should be a 1-cocycle, or something. Right? Because $z$ is changing too

#### Patrick Massot (Sep 18 2018 at 09:14):

oh yes, z is changing

#### Patrick Massot (Sep 18 2018 at 09:14):

I think it's not changing enough on my paper

Ok, it works now

#### Patrick Massot (Sep 18 2018 at 09:19):

You can continue to do number theory, it's alright

#### Patrick Massot (Sep 18 2018 at 09:19):

It was only a stupid copy-paste mistake

#### Johan Commelin (Sep 18 2018 at 09:20):

It also works on my paper

#### Johan Commelin (Sep 18 2018 at 09:20):

So, we've proven it! Let's move on to the next maths theorem (-;

#### Patrick Massot (Sep 18 2018 at 09:20):

It shouldn't be that hard to Lean (modulo those f***ing cast and coes)

#### Johan Commelin (Sep 18 2018 at 09:21):

Right, Kenny did a lot of useful stuff (-;

#### Johan Commelin (Sep 18 2018 at 09:21):

But all those actions of matrices on each other, and on the upper half plane...

#### Johan Commelin (Sep 18 2018 at 09:21):

That's going to be quite a pain.

#### Johan Commelin (Sep 18 2018 at 09:25):

@Patrick Massot Are you willing to take a shot at it?

#### Patrick Massot (Sep 18 2018 at 09:25):

I may try in the afternoon

#### Patrick Massot (Sep 18 2018 at 09:53):

I cleaned up a tiny bit but several things are weird. First I cannot sorry the proof. Lean complains there are remaining meta-variables, but I don't see where. And I have an hypothesis H: A ≈ B that I found no way to destruct into the existence of P in SL2 such that B = PA. This is not such a suprise because the beginning of the proof is really a mess

#### Patrick Massot (Sep 18 2018 at 09:54):

I think this is a very bad start. @Johannes Hölzl could you have a look?

#### Johan Commelin (Sep 18 2018 at 09:56):

Right... my brain stopped working after I wrote the start of that file. Guess why...

#### Johannes Hölzl (Sep 18 2018 at 10:04):

@Patrick Massot where should I look? I have no idea what a Hecke operator is. Did you push your commits, I don't see anything in kbb.

#### Johan Commelin (Sep 18 2018 at 10:05):

There is a file called Hecke_operator or something

#### Johan Commelin (Sep 18 2018 at 10:05):

The mathy definition is here: https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula

#### Johan Commelin (Sep 18 2018 at 10:06):

To prove that the sum is over a finite set, we need to use the stuff that you cleaned up.

#### Johannes Hölzl (Sep 18 2018 at 10:07):

Hm, the statements shouldn't change, besides reduce_def which is now reduce_eq1, reduce_eq2, reduce_eq3.

#### Johan Commelin (Sep 18 2018 at 10:12):

Right, line 12 should be

  haveI := SL2Z_M.finiteness m (ne_of_gt h),


#### Patrick Massot (Sep 18 2018 at 10:13):

Crap. I forgot to push

#### Patrick Massot (Sep 18 2018 at 10:14):

And I left my computer

Fixed

#### Patrick Massot (Sep 18 2018 at 10:40):

@Johannes Hölzl Now you can have a look, sorry about the false start

#### Johan Commelin (Sep 18 2018 at 10:52):

I'm a bit scared about the fact that we only know that SL2Z_H is a group action.

#### Johan Commelin (Sep 18 2018 at 10:52):

It seems like we would want to know that MAT2_H is a monoid action.

#### Patrick Massot (Sep 18 2018 at 10:53):

Oh yes, we need that

#### Johan Commelin (Sep 18 2018 at 10:53):

But refactoring SL2Z into a subtype of MAT2 give me a headache

#### Patrick Massot (Sep 18 2018 at 10:53):

I thought this was the reason you put det > 0 everywhere instead of det = 1

#### Johan Commelin (Sep 18 2018 at 10:53):

Because that means we have to go through all of Kenny's code again

#### Patrick Massot (Sep 18 2018 at 10:54):

And this is why I don't understand how term mode code could be easier to maintain

#### Johan Commelin (Sep 18 2018 at 10:54):

They set things up in the correct way the first time.

#### Patrick Massot (Sep 18 2018 at 10:54):

No, that's not what refactoring means

#### Johan Commelin (Sep 18 2018 at 10:54):

Instead of me: I only get it right after 42 attemts.

You're right.

#### Johan Commelin (Sep 18 2018 at 10:55):

But I agree that it is really confusing that we can not unfold that equivalence between A and B

#### Johan Commelin (Sep 18 2018 at 10:55):

After we have that, we could try to just battle on.

#### Johan Commelin (Sep 18 2018 at 10:55):

Although it might be nicer to have the monoid action do some work for us

#### Johan Commelin (Sep 18 2018 at 11:25):

Oh my goodness. If we want to generalise stuff to monoid actions there I'm so scared that everything breaks. I've learned a lesson: first try to think out some good API's.

#### Johan Commelin (Sep 18 2018 at 11:28):

@Johannes Hölzl So we have two problems: (1) how do we unfold the equivalence in hecke_operator.lean.

#### Johan Commelin (Sep 18 2018 at 11:29):

By definition A and B are equivalent if there is an M : SL2Z such that A = MB.

#### Johan Commelin (Sep 18 2018 at 11:29):

We want to get that M out.

#### Johan Commelin (Sep 18 2018 at 11:30):

And (2), to get a readable (and workable) version of the Hecke operator, it would be good to have A • z where A is any 2x2-matrix with integer coefficients, and z : ℍ.

#### Johan Commelin (Sep 18 2018 at 11:31):

In the end we will get (M • B) • z, and then we want to know that this is the same thing as M • (B • z)

#### Johannes Hölzl (Sep 18 2018 at 11:31):

So, first I fixed the basic definition. We currently had some missing goals (the anonymous constructor was outside tactic mode, so some type class instances where missing)

#### Johan Commelin (Sep 18 2018 at 11:35):

Ok, I guess that helps a bit (-;

#### Patrick Massot (Sep 18 2018 at 11:36):

I suspected something like this

#### Johan Commelin (Sep 18 2018 at 11:37):

@Johannes Hölzl Do you think it would be better if Möbius_transform turned into • notation?

#### Johannes Hölzl (Sep 18 2018 at 11:38):

Uh, overloading  •  could be problematic, at least annoying...

#### Johannes Hölzl (Sep 18 2018 at 11:38):

Why do we know that A an B are representatives?

#### Johannes Hölzl (Sep 18 2018 at 11:38):

so inreps?

#### Johan Commelin (Sep 18 2018 at 11:39):

No, we don't know that

#### Patrick Massot (Sep 18 2018 at 11:39):

We don't need that

#### Johan Commelin (Sep 18 2018 at 11:39):

They are merely "any representative"

#### Patrick Massot (Sep 18 2018 at 11:39):

This reps story is all used up in the finiteness fact

#### Patrick Massot (Sep 18 2018 at 11:39):

We won't use it again

in this proof

#### Johan Commelin (Sep 18 2018 at 11:40):

We won't use it again

We promise.

#### Johannes Hölzl (Sep 18 2018 at 11:40):

but we could use them to define the Hecke operator? Then we don't need to lift the quotients...

#### Johannes Hölzl (Sep 18 2018 at 11:40):

of course, later we need the proof anyway

#### Johan Commelin (Sep 18 2018 at 11:40):

Hmm, I suppose so.

#### Patrick Massot (Sep 18 2018 at 11:41):

That would be cheating

#### Johan Commelin (Sep 18 2018 at 11:41):

And "later" will be after the birthday party.

#### Johan Commelin (Sep 18 2018 at 11:43):

@Johannes Hölzl Why would we be overloading •? The monoid action MAT2 → ℍ → ℍ can be an instance of has_scalar right?

#### Johan Commelin (Sep 18 2018 at 11:43):

We don't have MAT2, but I think every monoid action should be an instance of has_scalar.

#### Johannes Hölzl (Sep 18 2018 at 11:43):

ah, okay. I thought you wanted to add another notation...

#### Patrick Massot (Sep 18 2018 at 11:43):

It's interesting to know how far one should be allowed to go into definition cheating. Say I want to prove RH in Lean. I define the usual zeta, call it zeta', and then define zeta(z) to be zeta'(z) if z is not a surprising zero of zeta', and one otherwise. Then I prove RH, and all is left is proving my definition of zeta is equivalent to the usual one...

#### Johannes Hölzl (Sep 18 2018 at 11:45):

what do you mean you want t get the M out? Like rintros A B ⟨M, eq⟩, works...

I guess so

#### Patrick Massot (Sep 18 2018 at 11:45):

I think it works because of your previous fix

#### Patrick Massot (Sep 18 2018 at 11:46):

It definitely didn't work this morning

Good!

#### Johan Commelin (Sep 18 2018 at 11:46):

Because now we can rw along eq, and then the fight begins!

#### Johannes Hölzl (Sep 18 2018 at 11:47):

The current state is

...
A B : Mat m,
M : SL2Z,
eq : SL2Z_M m M A = B,
weight_f :
∀ (M : SL2Z) (z : {x // x ∈ ℍ}),
f ⟨«Möbius_transform» ↑(M.a) ↑(M.b) ↑(M.c) ↑(M.d) ↑z, _⟩ =
(↑(M.c) * ↑z + ↑(M.d)) ^ (k + 1) * f z
⊢ 1 / (↑(A.c) * ↑z + ↑(A.d)) ^ (k + 1) *
f ⟨«Möbius_transform» ↑(A.a) ↑(A.b) ↑(A.c) ↑(A.d) ↑z, _⟩ =
1 / (↑(B.c) * ↑z + ↑(B.d)) ^ (k + 1) *
f ⟨«Möbius_transform» ↑(B.a) ↑(B.b) ↑(B.c) ↑(B.d) ↑z, _⟩


Is this what you want?

Yep

#### Johannes Hölzl (Sep 18 2018 at 11:47):

ah, okay. Its in kbb now

#### Johannes Hölzl (Sep 18 2018 at 11:50):

by the way: it is surely good style to define Möbius_transform on Mat m instead fof integer tuples.

#### Patrick Massot (Sep 18 2018 at 11:50):

I hate this integer tuples thing. I don't understand why we don't use matrices everywhere

#### Johan Commelin (Sep 18 2018 at 11:50):

Right, so why don't we define it on matrix (fin 2) (fin 2) R where R is a subring of ℝ?

#### Johan Commelin (Sep 18 2018 at 11:51):

Also, can we have a coercion from ℕ to fintype, that sends n to fin n?

#### Johan Commelin (Sep 18 2018 at 11:51):

Then stuff becomes even more readable (-;

#### Johan Commelin (Sep 18 2018 at 11:52):

@Patrick Massot I think we should. But with an old version of matrices it was hard to actually write down examples.

#### Johannes Hölzl (Sep 18 2018 at 11:53):

Hm, having a coerion from ℕ to Type would be nice!

#### Johannes Hölzl (Sep 18 2018 at 11:54):

Ah, I see there is SL2Z_H. So maybe we want a similar form for Mat m?

#### Johan Commelin (Sep 18 2018 at 11:54):

It is in the repo, but I haven't pushed yet.

#### Johan Commelin (Sep 18 2018 at 11:54):

Well, MAT2 really. And afterwards we can restrict to subtypes.

#### Johan Commelin (Sep 18 2018 at 11:54):

Mat m is a bad algebraic structure

#### Johan Commelin (Sep 18 2018 at 11:55):

It isn't a monoid

#### Johan Commelin (Sep 18 2018 at 12:09):

So, we have

@[simp] theorem one_val_ne {i j} (h : i ≠ j) : (1 : matrix n n α) i j = 0 :=
by simp [one_val, h]


in the matrices file. I would like Lean to try and figure out on its own if h is satisfied. In fin 2 it should know that 0 ≠ 1.

#### Johan Commelin (Sep 18 2018 at 12:09):

Is this something that an auto_param like dec_trivial could do?

#### Johannes Hölzl (Sep 18 2018 at 12:09):

Okay, I added M_trans anyway.

#### Johan Commelin (Sep 18 2018 at 12:10):

How do I need to change the statement?

#### Johannes Hölzl (Sep 18 2018 at 12:11):

Either add a tactic: dec_tac := [exact dec_trivial] and use this: (h : i ≠ j . dec_tac)

#### Johannes Hölzl (Sep 18 2018 at 12:11):

or use default parameter (h : i ≠ j := dec_trivial)

#### Johannes Hölzl (Sep 18 2018 at 12:12):

I don't know if the default parameter work. If dec_trivial gets evaluated too early it might not work

I'll try.

#### Johan Commelin (Sep 18 2018 at 12:13):

Ok, the M_trans is nice. So now we need to plug that into the definition of the Hecke operator.

#### Johan Commelin (Sep 18 2018 at 12:15):

It isn't happy about meta def dec_tac : tactic unit := [exact dec_trivial]

#### Johannes Hölzl (Sep 18 2018 at 12:16):

meta def dec_tac : tactic unit := [exact dec_trivial]


maybe?

That worked

#### Johan Commelin (Sep 18 2018 at 12:19):

So now my goal is:

z : ℂ
⊢ (z + ↑0) / (1 + ↑0 * z) = z


If Kevin saw that goal...

#### Johan Commelin (Sep 18 2018 at 12:19):

simp didn't kill it.

#### Johannes Hölzl (Sep 18 2018 at 12:19):

Does unfold_coes help?

#### Johan Commelin (Sep 18 2018 at 12:21):

Is that a tactic?

yes

#### Johan Commelin (Sep 18 2018 at 12:24):

It doesn't help enough...

#### Johan Commelin (Sep 18 2018 at 12:25):

I'll go back to the Hecke operator for a moment.

#### Johan Commelin (Sep 18 2018 at 14:59):

Ok guys... I'm gone for a week. I might be able to check Zulip now and then, but I won't be able to do any serious Leaning until next week on Thursday.

#### Johan Commelin (Sep 18 2018 at 14:59):

I'm looking forward to Kevin's reaction on Friday

#### Johan Commelin (Sep 18 2018 at 14:59):

Thanks for all your help so far! I really enjoyed it!

#### Patrick Massot (Sep 18 2018 at 14:59):

But we still haven't decided what will happen on Friday

#### Patrick Massot (Sep 19 2018 at 09:21):

Seriously, what are we doing tomorrow? @Chris Hughes will you see Kevin tomorrow?

#### Johan Commelin (Sep 19 2018 at 09:28):

Tomorrow is Thursday. I guess any cleaning up that we want to do should be done today or tomorrow. On Friday we give Kevin access to kbb and we PR the determinants file and the remainder of matrices.lean

#### Johan Commelin (Sep 19 2018 at 09:29):

I don't think there is much in the modular form files that is ready to merge.

#### Chris Hughes (Sep 19 2018 at 09:30):

What about sin and cos? We don't have pi yet, but we do have sin and cos.

#### Patrick Massot (Sep 19 2018 at 09:30):

I would veto the current definition of sin

#### Patrick Massot (Sep 19 2018 at 09:30):

unless it changed recently

How come?

#### Johan Commelin (Sep 19 2018 at 09:30):

What was wrong with it?

#### Patrick Massot (Sep 19 2018 at 09:31):

Would you write this on a blackboard?

#### Patrick Massot (Sep 19 2018 at 09:31):

def sin (z : ℂ) : ℂ := ((exp (-z * I) - exp (z * I)) * I) / 2

come on

#### Kenny Lau (Sep 19 2018 at 09:31):

I don't see what's wrong with it

#### Patrick Massot (Sep 19 2018 at 09:32):

Is it the definition in the UK?

#### Johan Commelin (Sep 19 2018 at 09:32):

I think a PR on exp would be nice. Possibly including cos und sin. Hopefully that will induce a rampage by some Lean-fu experts to prove continuity.

#### Johan Commelin (Sep 19 2018 at 09:32):

I don't even know what definition of sin I saw. My training in analysis was terrible.

#### Johan Commelin (Sep 19 2018 at 09:33):

Possibly it was the analytic continuation of real.sin

#### Johan Commelin (Sep 19 2018 at 09:33):

I don't know how real.sin was defined. Probably using angles etc...

#### Chris Hughes (Sep 19 2018 at 09:33):

I'm going to have a serious bash on continuity today. The definition I saw was ((exp (z * I) - exp (-z * I))) / (2 * I)

#### Patrick Massot (Sep 19 2018 at 09:33):

In France, sin z = (exp (z * I) - exp (-z * I)) * I) / (2*I)

#### Kenny Lau (Sep 19 2018 at 09:34):

is there any difference?

#### Patrick Massot (Sep 19 2018 at 09:34):

Yes. One is the definition people expect to see, the other one could be a useful lemma if Chris needs it

#### Chris Hughes (Sep 19 2018 at 09:34):

I multiplied by $-i$, Patrick divided by $i$.

#### Patrick Massot (Sep 19 2018 at 09:35):

Chris, why did you do that?

#### Chris Hughes (Sep 19 2018 at 09:36):

It's easier to prove sin (x + y) because I have less division to deal with.

#### Patrick Massot (Sep 19 2018 at 09:36):

Then you could use a lemma

#### Patrick Massot (Sep 19 2018 at 09:36):

Actually I don't understand why you use these proofs for sin(x+y) etc.

#### Chris Hughes (Sep 19 2018 at 09:37):

Which proofs should I use?

#### Patrick Massot (Sep 19 2018 at 09:37):

Why not taking real and imaginary parts of the equation exp(i(x+y)) = exp(ix)exp(iy)?

#### Patrick Massot (Sep 19 2018 at 09:37):

That's the real life proof

#### Patrick Massot (Sep 19 2018 at 09:38):

But I guess you should rather prove continuity and try to get pi

#### Patrick Massot (Sep 19 2018 at 09:38):

And also answer my question: will you see Kevin tomorrow?

Yes.

#### Johan Commelin (Sep 19 2018 at 09:42):

@Patrick Massot Why tomorrow? Don't you mean Friday? Or do you have some plan in mind?

#### Chris Hughes (Sep 19 2018 at 09:43):

I won't see him on Friday.

#### Johan Commelin (Sep 19 2018 at 09:44):

@Scott Morrison Could you give Kevin access when it is Friday 09:00 your time? Because then it is 00:00 his time, I think.

Sure.

Nice :lol:

#### Patrick Massot (Sep 19 2018 at 09:54):

I meant Friday, sorry

#### Johan Commelin (Sep 19 2018 at 09:55):

And @Kenny Lau isn't back in the UK at that point, I guess?

i'm not

#### Johan Commelin (Sep 19 2018 at 09:55):

Patrick, were you thinking of physically giving him some gift? A print-out of the files :lol: ?

#### Patrick Massot (Sep 19 2018 at 09:57):

I wanted someone who could see his face and tell us.

#### Johan Commelin (Sep 19 2018 at 09:58):

Agreed, that would be nice.

#### Mario Carneiro (Sep 19 2018 at 16:17):

Why not taking real and imaginary parts of the equation exp(i(x+y)) = exp(ix)exp(iy)?

That only proves the addition formulas for sin and cos when the arguments are real

oh yes

#### Mario Carneiro (Sep 19 2018 at 16:18):

I don't think there is any substitute for just doing the algebra in the complex case

#### Patrick Massot (Sep 19 2018 at 16:18):

I never thought about the complex case here

crazy

#### Reid Barton (Sep 19 2018 at 16:35):

no problem. then just show that two holomorphic functions which agree on the real line are equal :upside_down:

Great !

#### Johan Commelin (Sep 20 2018 at 22:27):

This is so amazing! Awesome! That was an immense tour de force, Chris. Well done!

#### Johan Commelin (Sep 20 2018 at 22:30):

I am about to go to bed. I'm sorry I won't be able to be online when Kevin gets his birthday present. I am sure that you guys will be able to break the surprise! I'll read up on it afterwards (-;

#### Scott Morrison (Sep 20 2018 at 22:36):

I think the plan is that in 24 minutes I will add Kevin to the kbb repository.

#### Johan Commelin (Sep 20 2018 at 22:48):

@Scott Morrison Yes, that's a good plan!

#### Johan Commelin (Sep 20 2018 at 22:48):

You can also add him to this stream on Zulip, and you can write a happy birthday post in the general stream.

#### Johan Commelin (Sep 20 2018 at 22:49):

I should really go to bed now. Tomorrow I'll have 4 hard math-talks waiting for me...

Happy PR'ing (-;

wtf?

#### Johan Commelin (Sep 21 2018 at 05:15):

@Kevin Buzzard We hope you will enjoy reading back through all our crazy conversations of the last 10 days. :stuck_out_tongue_wink:

#### Simon Hudon (Sep 21 2018 at 05:16):

Did we bash Kevin in any of it?

#### Patrick Massot (Sep 21 2018 at 06:49):

I don't remember doing it more than on the regular streams

#### Patrick Massot (Sep 21 2018 at 06:51):

Kevin: the conversation about this project started in group PM but then it was generating a huge mess of notification for everybody, and I eventually found out anybody could create private streams. So the story of this stream starts in the middle.

#### Patrick Massot (Sep 21 2018 at 06:55):

I think it's fair to point out that Johan came with this idea, on September 4th.

#### Patrick Massot (Sep 21 2018 at 06:57):

In order to understand the mess in the repository, it may be relevant to know that, beyond Johan's idea of a birthday pi, the unrealistic idea that I proposed was to formal abstract https://www.sciencedirect.com/science/article/pii/S0022314X96900396?via%3Dihub

ROFL

#### Kevin Buzzard (Sep 21 2018 at 11:09):

That is so funny. That is a fine abstract to formalise. It would be trivial if there was a half-decent API for modular forms, and Lean is perfect for that sort of thing.

#### Kevin Buzzard (Sep 21 2018 at 11:11):

You could formalise a mathematically equivalent statement more easily -- the eigenvalues of a Hecke operator on a space of modular forms are the same as the eigenvalues of a corresponding Hecke operator on a certain group cohomology group, by a theorem of Eichler and Shimura. Formalising group cohomology would perhaps be easier than formalising modular forms -- I'm not really sure but it sounds easier to me. Group cohomology is just there waiting to be done.

#### Kevin Buzzard (Sep 21 2018 at 11:13):

I wrote that paper after hearing a talk of Dinakar Ramakrishnan, when he mentioned that he had never seen a modular eigenform whose Hecke eigenvalues generated a non-solvable extension of the rationals. Talking to him afterwards it became clear that this was only because there were no computer programs to compute modular forms, and that we all knew exactly where to look. I took the trouble to look and there they were. Dinakar urged me to write it up.

#### Patrick Massot (Sep 21 2018 at 11:25):

We are not so far away from having Hecke operators (they almost act on functions of a fixed weight, and it shouldn't be so hard to show they act on holomorphic functions and preserve boundedness at infinity). We also have characteristic polynomial, and Johannes has been working towards Galois groups. But we mostly gave up when Johan pointed out that we would need that modular forms of a fixed weight form a finite dimensional subspace of holomorphic functions (we do have a vector space structure on holomorphic functions on the upper half plane).

#### Kevin Buzzard (Sep 22 2018 at 09:43):

aie, yes, finite-dimensionality is needed. A trivial consequence of the fact that the global sections of a line bundle on a compact Riemann surface are finite-dimensional, so by maths_undergraduate should do it. I'm going to try and build that tactic at Imperial.

Finite-dimensionality for the group cohomology would be a trivial consequence of the fact that a finite index subgroup of a finitely-generated group is finitely-generated, and the fact that SL(2,Z) is finitely-generated. I don't know how easy it is to prove the finite index result just by group theory, I am no algebraist. The proofs I know are topological. The group cohomology variant would be provably equal once we had something like Stokes' theorem.

#### Johan Commelin (Sep 22 2018 at 10:31):

We have the fact that S and T generate SL2Z in your birthday repo :lol:

#### Kevin Buzzard (Sep 22 2018 at 11:37):

Right. But for finite-dimensionality of the cohomology group for general levels we'll need that a finite index subgroup of a f.g. group is f.g. But I see what you're saying -- this is enough to prove that level 1 modular forms are finite-dimensional.

#### Kevin Buzzard (Sep 22 2018 at 11:37):

There is some kind of subtlety which I have only recently become aware of, and again it was a comment of @Reid Barton which clarified things for me. Without some general theory of global sections of line bundles on compact Riemann surfaces it's kind of a pain to prove that the space of modular forms is finite-dimensional. But it is finite-dimensional, so one can define the char poly of a Hecke operator to be "if the space is infinite-dimensional then 37, and if it's finite-dimensional then the char poly". This gives a sorry-free way of defining the char poly which is human-provably equivalent to the right thing. What one cannot do is to get away without defining the Hecke operator at all and just sorrying it -- because then the char poly has a sorry in too.

One of the things I realise I want now is for a bunch of mathematicians to come along and say "can you formalise theorem X or definition Y in Lean?" because questions such as that are ways of discovering what kind of an API a normal mathematician (perhaps with no Lean training) wants. Who cares about proofs, they are too hard. I know that Mario feels that a definition is pointless without an application. How about if the application is some statements of theorems or conjectures?

Last updated: May 18 2021 at 10:14 UTC