Zulip Chat Archive

Stream: kbb

Topic: hecke operator


view this post on Zulip Johan Commelin (Sep 14 2018 at 16:32):

The next step would be to define https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula on the subspace of Petersson_weight k functions on the upper half plane.

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:33):

Afterwards, we need to show that it preserves holomorphic, bounded_at_infinity and zero_at_infinity.

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:33):

We also need to prove that it is linear.

view this post on Zulip Johan Commelin (Sep 14 2018 at 18:55):

Ok, this stuff is a mess. I just wanted to plug a matrix with determinant m into the Möbius transform action. Of course that doesn't work...

view this post on Zulip Kenny Lau (Sep 14 2018 at 19:04):

wow this is really a heck of an operator

view this post on Zulip Johan Commelin (Sep 14 2018 at 19:13):

Ok, I think we should forget about Hecke operators. We can define them if we want. But we won't even get close to formalising the abstract of Kevin's paper.

view this post on Zulip Johan Commelin (Sep 14 2018 at 19:13):

Until 5 minutes ago, I thought that the only thing missing was the fact that SkS_k is finite-dimensional (which requires Riemann–Roch).

view this post on Zulip Johan Commelin (Sep 14 2018 at 19:15):

But of course, with the definition of the Hecke operator that we are now going after, we will get a linear operator on a complex vector space. This beast will have a characteristic polynomial defined over complex.

view this post on Zulip Johan Commelin (Sep 14 2018 at 19:15):

Such polynomials do not have very interesting splitting fields.

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:30):

How do you prove this polynomial has interesting coefficients in the real world?

view this post on Zulip Reid Barton (Sep 15 2018 at 13:32):

are the coefficients actually rational?

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:32):

I guess there are integers

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:32):

But I know no number theory

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:34):

And it probably also requires Fourier series for modular forms

view this post on Zulip Reid Barton (Sep 15 2018 at 13:35):

If they are actually integers, then can't we define the splitting field to be the smallest subfield of C which contains the roots?

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:36):

The Hecke operator acts on the singular homology of the modular curve. This has Q coeffients

view this post on Zulip Reid Barton (Sep 15 2018 at 13:36):

Then we don't need either splitting fields or to prove that the coefficients are integers

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:36):

By Hodge theory you recover the cusp forms in the complexification of this cohomology group.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:36):

But maybe I'm using a sledgehammer, there might be a more low-brow proof.

view this post on Zulip Reid Barton (Sep 15 2018 at 13:37):

Of course then we wouldn't know that the this field is a finite extension...

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:37):

Right...

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:38):

Somehow I don't mind sorrying finite-dimensionality of S_k, but sorrying this fact feels like a big cheat.

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:39):

I guess Hecke's point of view was less sophisticated

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:41):

Probably. I think using Fourier coefficients there is another approach.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:42):

But then, we didn't want to do Fourier coefficients either.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:42):

So maybe we just define the Hecke operator over complex, and then wrap up the project.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:35):

Let's put this discussion in the correct thread.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:35):

The following lemma is crucial:

theorem M_trans_SL2Z_H {m : } {h : m > 0} {M : SL2Z} {A : Mat m} :
M_trans h (SL2Z_M m M A) = SL2Z_H M  (M_trans h A) :=
begin
  funext z,
  simp [M_trans, SL2Z_M, SL2Z_H, «Möbius_transform»],

-- m : ℤ,
-- h : m > 0,
-- M : SL2Z,
-- A : Mat m,
-- z : ↥ℍ
-- ⊢ (↑(M.a) * ↑(A.b) + (↑(M.b) * ↑(A.d) + (↑(M.a) * ↑(A.a) + ↑(M.b) * ↑(A.c)) * ↑z)) /
--       (↑(M.c) * ↑(A.b) + (↑(M.d) * ↑(A.d) + (↑(M.c) * ↑(A.a) + ↑(M.d) * ↑(A.c)) * ↑z)) =
--     (↑(M.b) + ↑(M.a) * ((↑(A.b) + ↑(A.a) * ↑z) / (↑(A.d) + ↑(A.c) * ↑z))) /
--       (↑(M.d) + ↑(M.c) * ((↑(A.b) + ↑(A.a) * ↑z) / (↑(A.d) + ↑(A.c) * ↑z)))

  -- ring, -- fails
end

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:36):

I'm not surprised that ring fails, because there are divisions. But boy, I really don't want to prove this stuff by hand.

view this post on Zulip Patrick Massot (Sep 18 2018 at 12:36):

I could try since Johannes is working for me right now

view this post on Zulip Patrick Massot (Sep 18 2018 at 12:36):

Did you push everything?

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:37):

Hm, isabelle has field_simps for these kind of things. field_simps is a collection which applies distributivity, and tries to remove the x / d. Sometimes it needs to introduces if to check if d = 0

view this post on Zulip Patrick Massot (Sep 18 2018 at 12:38):

We need this so badly

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:45):

I pushed some stuff

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:45):

I've got M out of f, so now we need to do the cocycle computation

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:46):

Which is just as ugly as the other thing I just posted.

view this post on Zulip Patrick Massot (Sep 18 2018 at 12:46):

Did you do the other ugly thing?

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:55):

No, everything I did was pushed.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:55):

I went to the last sorry: proving that the result again has weight k

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:55):

I now have the following goal

 quotient.lift_on' o
      (λ (A : Mat m), 1 / ((A.c) * (SL2Z_H M z) + (A.d)) ^ (k + 1) * f.val (M_trans h A (SL2Z_H M z)))
      _ =
    ((M.c) * z + (M.d)) ^ (k + 1) *
      quotient.lift_on' o (λ (A : Mat m), 1 / ((A.c) * z + (A.d)) ^ (k + 1) * f.val (M_trans h A z)) _

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:55):

How do I get past that quotient.lift_on'?

view this post on Zulip Patrick Massot (Sep 18 2018 at 12:55):

I'm working on M_trans_SL2Z_H

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 13:04):

eliminate o. Easiest: rcases o with <x>.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:09):

Thanks, that worked!

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:09):

@Patrick Massot The name is wrong. The final _H should be _M.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:09):

With _H it is another lemma, and I need that one now (-;

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:10):

but do you still want {m : ℤ} {h : m > 0} {M : SL2Z} {A : Mat m} : M_trans h (SL2Z_M m M A) = SL2Z_H M ∘ (M_trans h A)?

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:10):

Or only the other one?

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:12):

No, the one you are working on is used

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:12):

I just realised that I had the wrong name.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:12):

You can already see it being used

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:13):

In what I last pushed

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:36):

Aaahrg, the final sorry is a real pain. I'm now even confused about the maths again.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:37):

OTOH, those are the better moments of theorem proving (-; I'm rather confused about the maths than that I'm fight silly

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:44):

I just pushed something

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:45):

Things are reduced to many variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/hecke_operator.lean#L16 which itself is a variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/upper_half_space.lean#L37

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:45):

But I'm tired of fighting this

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:46):

After writing https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/hecke_operator.lean#L32-L49

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:46):

One day we will think back and laugh. But right now it's only screaming: Lean is nowhere near ready!

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:47):

Right, it's really annoying

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:51):

I also pushed. I didn't really get very far.

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:52):

Maybe we can switch sides

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:53):

So, on my side that maths is confusing.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:53):

If you take an f of weight k. After you plug it into Hecke, you want to check that the result has weight k.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:54):

But this means that you get f(A • M z), where A : Mat m and M : SL2Z

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:54):

Now you can't use the weight property of f.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:54):

Because the M is not on the left.

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:55):

But A M A¯¹ doesn't have to be in SL2Z...

view this post on Zulip Johan Commelin (Sep 18 2018 at 13:55):

So now I'm confused.

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:56):

M should be on the left

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:56):

We are acting from the left

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:56):

At least on my piece of paper

view this post on Zulip Patrick Massot (Sep 18 2018 at 13:56):

And on Wikipedia

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:00):

Yes, but M acts before A does, right?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:01):

It is f (A • (M • z)). So M is in fact acting on the left.

view this post on Zulip Reid Barton (Sep 18 2018 at 14:02):

Yeah you want to write AM=MAAM = MA' for some other AA' of det m, I think. The action of M will permute the terms of the sum

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:02):

It didn't seem necessary earlier today

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:04):

I think using reflexivity of the equivalence relation is enough

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:04):

or reflexivity of equality

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:05):

Hmmm... Reid, that might be the trick

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:05):

I tried writing AM = M'A, but then your M' is not in SL2Z

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:05):

But maybe with your attack it works.

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:06):

You need to prove to compute the term in the sum corresponding to AM until you get the one corresponding to M

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:06):

Because A=M1AMA' = M^{-1}AM and M1SL2ZM^{-1} \in \mathrm{SL2Z}

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:07):

@Patrick Massot I don't think that will work. You really need to use that f has weight k at some point. So you need to rewrite things.

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:07):

of course you use that!

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:07):

Ok, then I'm confused about your plan.

view this post on Zulip Reid Barton (Sep 18 2018 at 14:10):

The book I have writes the action of SL(2, Z) (or more generally GL+(2, R)) on functions on the upper half plane as a right action, which I think makes more sense

view this post on Zulip Reid Barton (Sep 18 2018 at 14:10):

(fkγ)(z)=detγ(cz+d)kf(γz)(f|_k \gamma)(z) = \frac{\det \gamma}{(cz + d)^k} f(\gamma z)

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:12):

True, but it acts on the left on the plane, right?

view this post on Zulip Reid Barton (Sep 18 2018 at 14:12):

and also the Hecke operators
(fkTp)=pk/21δfkδ(f|_k T_p) = p^{k/2-1} \sum_\delta f|_k \delta "where δ\delta runs over a set of representatives for the distinct right cosets of Γ1(N)\Gamma_1(N) in Δp\Delta_p"

view this post on Zulip Reid Barton (Sep 18 2018 at 14:12):

Yes

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:13):

In Lean we only have the action on the plane, so far...

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:13):

Well, and the action on other matrices.

view this post on Zulip Reid Barton (Sep 18 2018 at 14:14):

Then to check that the Hecke operator preserves modular forms of weight k you need to show that
(δfkδ)kγ=δfδ(\sum_\delta f|_k\delta)|_k \gamma = \sum_\delta f|_\delta and the strategy is going to be to move γ\gamma past δ\delta and reindex

view this post on Zulip Reid Barton (Sep 18 2018 at 14:17):

Yeah, I'm just trying to show how to isolate the step where you reindex the sum

view this post on Zulip Reid Barton (Sep 18 2018 at 14:19):

do we even know yet that the Hecke operator preserves holomorphic functions?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:20):

That statement does not make sense yet (-;

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:20):

Hmmm, maybe we could turn it into a sensible statement.

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:20):

At the moment the Hecke operators are being defined as operators on functions of weight k

view this post on Zulip Reid Barton (Sep 18 2018 at 14:21):

do we know that (az + b)/(cz + d) is itself a holomorphic function?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:21):

Afterwards we want to check that the preserve holomorphic functions and functions bound at infinity.

view this post on Zulip Reid Barton (Sep 18 2018 at 14:21):

right

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:21):

We do not know that

view this post on Zulip Reid Barton (Sep 18 2018 at 14:21):

I see

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:21):

It might be a nice example of a holomorphic function (-;

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:24):

are there any sorry that I can fill in?

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:24):

YES

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

@Kenny Lau It might be good to read the discussion of the last 20 minutes

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:25):

There is some non-trivialish math going into this. (Nothing you don't understand in 30 secs) But still...

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:26):

where is the sorry?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:27):

Look in the Hecke file

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:27):

is it WIP?

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:27):

I don't want to cause pull conflict

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:29):

I stand by my claim we don't need any reordering

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

I'm not working on it right now

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

Need to do some emails

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:29):

Hold on 10 sec

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:31):

Ok, look at https://github.com/semorrison/kbb/blob/master/src/hecke_operator.lean#L76

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:31):

I claim there is no problem here

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:31):

Except we miss a field tactic

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:32):

Kenny: you can fill in all sorries in that file

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:32):

well you just pulled

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:32):

pushed*

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:32):

yes

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:32):

Don't forget what I wrote: Things are reduced to many variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/hecke_operator.lean#L16 which itself is a variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/upper_half_space.lean#L37

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:32):

About the other sorries in that file

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:33):

And if you really feel like impressing us, you can get rid of all quadruples of integers and use matrices everywhere

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:33):

I'm giving up on this.

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:34):

Honestly I think the upshot of this story is that Lean is not yet ready for anything involving divisions

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:35):

I don't feel like impressing anyone

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:35):

You could always just apply division cancellation theorems, it's not that hard...

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:35):

Mario, did you see https://github.com/semorrison/kbb/blob/master/src/hecke_operator.lean#L32-L49?

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:35):

I'm not too keen on replacing these direct and logical proofs with arcane tactic-generated proofs

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:36):

The trouble with division cancellations theorems is that terms must be next to each other

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:36):

I am very keen on have a tactic that will write the direct and logical proof for me.

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:36):

hence the endless conv

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:36):

No, this is stupid

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:36):

We don't want to see this proof

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:37):

We want Lean to compute, as with ring

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:37):

I think it can be done better than that

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:37):

plus a little calc would go a long way in that proof

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:37):

what is all the uparrow stuff?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:38):

ℤ-matrices acting on ℂ

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:39):

There is a boatload of stuff in this repo that could be generalised. But some thing's can't... for example this lemma could be about arbitrary matrices in GL2R+. But that would shift the arrows somewhere else.

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:47):

I'm looking forward to Lean Forward... these things are the basic Lego blocks that Sander Dahmen works with.

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:48):

Okay, I've downloaded and set up kbb. What area needs my attention?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:48):

hecke_operator.lean

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:48):

You'll get pulled into the other files by import

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:48):

Beware, there are minor dragons in these files.

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:49):

Every 10 lines will give you another opportunity for a major refactor (-;

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:49):

The area where you write a field tactic

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:49):

@Kenny Lau you might want to tell @Mario Carneiro which sorry you are working on.

view this post on Zulip Kenny Lau (Sep 18 2018 at 14:50):

all of them

view this post on Zulip Mario Carneiro (Sep 18 2018 at 14:50):

lol that's not happening before friday Patrick

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:50):

I'm sure Kevin will understand

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:51):

Do you think you could do it before he turns 60?

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:51):

@Mario Carneiro Any improvements of the repo would be appreciated.

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:51):

matrices and determinants seem to be almost ready to merge. And independent of the other files.

view this post on Zulip Kenny Lau (Sep 18 2018 at 15:19):

@Patrick Massot what's the math proof of the thing that Patrick claims to be true?

view this post on Zulip Kenny Lau (Sep 18 2018 at 15:20):

and what is the second thing?

view this post on Zulip Patrick Massot (Sep 18 2018 at 15:20):

The maths proof is to expand everythings and compute

view this post on Zulip Patrick Massot (Sep 18 2018 at 15:20):

But probably there is a better way to setup all this

view this post on Zulip Kenny Lau (Sep 18 2018 at 15:22):

I filled in two of the sorries

view this post on Zulip Kenny Lau (Sep 18 2018 at 15:22):

see if you can learn anything therefrom

view this post on Zulip Johan Commelin (Sep 19 2018 at 10:15):

Reid quoted some formulas containing the Petersson slash operator (of weight k). Would it make sense to mimic that notation, somehow? I think we should also wrap M_trans and SL2Z_H into notation (has_scalar). I hope it will make statements more readable. Maybe it will even improve proofs, I don't know.

view this post on Zulip Johan Commelin (Sep 19 2018 at 11:04):

@Kenny Lau I agree with Patrick's claim. I made some small rewrites. Maybe now it is easier to math-see why it is true. I still wish ring would kill this. But it doesn't... because there are divisions. I hate divisions in Lean.

view this post on Zulip Johan Commelin (Sep 19 2018 at 11:05):

(Oooh, I also pushed those small rewrites.)


Last updated: May 18 2021 at 09:14 UTC