constants

Stream: condensed mathematics

[Johan Commelin]

I just pushed a whole load of changes. In particular, I think thm95/constants.lean now contains all the inequalities that the sorryd constants should satisfy.

[Johan Commelin]

So I you love defining 8 constants in a mutually inductive definition, please attack that file :octopus:

[Adam Topaz]

Can we set gptf loose on that file for three weeks and see what happens?

[Johan Commelin]

Current sorry count:

3       src/prop819.lean
15      src/thm95/col_exact.lean
12      src/thm95/constants.lean
2       src/prop819/locally_constant.lean
Total:  32

[Johan Commelin]

In particular, the col_exact part of the main proof (thm95/default.lean) has been filled in, but of course it still depends on prop819 and the stuff in thm95/col_exact.lean.

[Peter Scholze]

I'm looking forward to seeing the final constants!! In particular, I wonder how far off my guess of double-exponential growth (of k in terms of m) was.

Towards the end of the file, there's a squareroot of k_1appearing if I understand it right. Where is that coming from?

[Jesse Michael Han]

Adam Topaz said:

Can we set gptf loose on that file for three weeks and see what happens?

we're in the middle of training a new model on updated mathlib + lean-liquid! cc @Stanislas Polu

no promises about being able to synthesize mutual inductives but the new model should know a lot more condensed mathematics

[Johan Commelin]

Peter Scholze said:

Towards the end of the file, there's a squareroot of k_1appearing if I understand it right. Where is that coming from?

The "dual" snake lemma, I think.

[Peter Scholze]

OK

[Johan Commelin]

It says that if $M \to N \to P$ and $N$ and $P$ are weak exact with constant $k$, then $M$ is weak exact with constant $k^2$.
So we need to prove that the column $N$ (before taking $T^{-1}$-invariants) is weak exact with constant $\sqrt{k_1}$.

[Peter Scholze]

Shouldn't it be rather easy to fill in those sorry's? I mean you want to define a new number $x$ such that some inequalities $a\leq x, b\leq x, c\leq x$ hold. Can't you just define $x=\mathrm{max}(a,b,c)$?

[Johan Commelin]

Yes, it will be something like that.

[Peter Scholze]

In any case, the requirements do look like what I imagined. And it seems to confirm a bound of the form $k=O(C^{3^{m^2}})$ and $K=O(C(r,r')^{3^{m^2}})$ for some absolute constant $C$ (maybe $C=3$ or so) and some simple explicit function $C(r,r')$ of the radii.

[Johan Commelin]

mathlib even has big-O (-;

[Johan Commelin]

So we could potentially verify your claims (-;

[Kevin Buzzard]

Heh, so I just spent some time looking at that file and came to the same conclusion as Peter. I killed the sqrt sorry.

[Kevin Buzzard]

But it seems to me that one could kill all the sorries by defining K₁ (m+1) to be the max of 1 and K BD c' r r' m etc

[Peter Scholze]

Don't forget K1_spec, but yes

[Kevin Buzzard]

Oh so I just started filling them in and it's harder than I thought :-) When defining k_1: k_0 depends on k_1 and k' depends on k_0 and k depends on k' and now I want some inequality between k_1 and k', so one does actually have to think a little.

[Peter Scholze]

Hmm so I guess the reason is that in this inductive scheme, it's not obvious to Lean that to define k c' (m-1) one has only ever used the values of k1 m' for $m'\leq m-1$, so it's fine to define k1 m = k c' (m-1) ?

[Peter Scholze]

But I'd think one only needs to spell out what k c' (m-1) is to see that this is the case

[Kevin Buzzard]

Right, one has to think a little about how to do this without doing a "mutually inductive definition", which is exactly what Johan was talking about earlier. Note that there are also constants c'(0), c'(1),... involved, and these seem to have no definition.

[Peter Scholze]

In general not, but for Johan's example of BD data, they ought to be explicit

[Johan Commelin]

Yeah, it's fine to abstract over c'

[Johan Commelin]

Otherwise you'll just get a whole bunch of powers of 2 thrown in the mix.

[Peter Scholze]

How large are the c'in your example?

[Johan Commelin]

I haven't checked carefully, but something roughly like 2 ^ n, I think

[Peter Scholze]

OK, so "small" ;-)

[Johan Commelin]

Right, they shouldn't get close to doubly exponential at all.

[Johan Commelin]

Note that the 4 sorrys all the way at the bottom of the file have "nothing" to do with the big tangled mess of the rest of the file.

[Johan Commelin]

So filling them in is an independent task, and probably quite a lot easier.

[Scott Morrison]

thm95/default.lean wasn't compiling because k₁ now has an explicit dependence on c'; I've fixed this.

[Kevin Buzzard]

Oh sorry, that was my fault. But it does depend on c'!

[Scott Morrison]

If you were allowed to assume a few inequalities are strict in c₀_spec those last four inequalities are easy to deal with. But either of k₁_sqrt c' m = 1 or c_ j = 0 makes it nontrivial, because then you can't just make c₀ big enough.

Can we tweak k₁ so we're allowed to know that it is strictly greater than 1?

Where can I get c_ j \ne 0 from?

[Scott Morrison]

Perhaps _inst_8: package.adept BD c_ c' tells you this? (I'm quickly revealing my ignorance. :-)

[Scott Morrison]

Nothing seems to go wrong if we tweak the definition of k₁ so it is strictly greater than 1, but I don't feel confident pushing that, without better sense of whether it could make other things harder.

[Johan Commelin]

@Scott Morrison You can assume c_ j > 0

[Scott Morrison]

Great --- where will that come from, I'm curious now!

[Johan Commelin]

Well, I've also assumed in the breen_deligne/constants.lean when I construct c' from c_

[Johan Commelin]

And the example BD constants satisfy that condition.

[Johan Commelin]

So we can add it as a condition to breen_deligne.very_suitable BD c_.

[Johan Commelin]

But since BD is not an out_param in the def (it could be!) type class inference will not be able to find fact (0 < c_ j) automatically.

[Johan Commelin]

If c_ j = 0 we get some very degenerate behaviour. Really, what we are interested in is the successive quotients c_ j / c_ (j+1) which should bound the operator norm of BD.d (j+1) j.

[Johan Commelin]

So then it's quite clear that morally they should be invertible even if Lean doesn't force us to assume this.

[Johan Commelin]

Similarly, k_1 will always be > 1, so we can also get k_1_sqrt to be > 1.

[Scott Morrison]

Hmm, something is not right in those last four sorries. c₀_spec involves c_ j, but there isn't any argument that constrains it in any way, so making the c_ j too small would break the inequality.

[Johan Commelin]

j <= m, should be there.

[Johan Commelin]

So there are only finitely many of them involved.

[Scott Morrison]

Sure. But as written c₀ is not allowed to know what c_ is at all.

[Scott Morrison]

Is that a mistake?

[Johan Commelin]

Oooh, I see. Sorry. Yes, it is allowed to know that.

[Johan Commelin]

If you assume 1 < k_1_sqrt, does that allow c_ j = 0? Because that would be a lot less refactoring (-;

[Johan Commelin]

Alternatively, just assume [\all j, fact (0 < c_ j)] and I will just pass that assumption around using TC.

[Scott Morrison]

No, I need both separately, as far as I can see.

[Johan Commelin]

Ok, I'm adding 0 < c_ j as condition to very_suitable. Expect a push in a couple of moments.

[Johan Commelin]

Aahrg, that constant isn't really becoming nicer to write down: c₀ BD r r' c_ c' Λ m

[Johan Commelin]

But ey... it seems to work.

[Johan Commelin]

@Scott Morrison I pushed

[Patrick Massot]

Scott, if you work on this, you should also have a look at those lines I added yesterday. The point is I think expliciting functions b and N2 will help untangle things. They no longer need to be part of the inductive definition, they are simply standalone functions.

[Johan Commelin]

I think Scott was mainly look at $c_0$, which should be independent of the tangle above it.

[Peter Scholze]

Yes, please make everything as explicit as possible!

[Johan Commelin]

Just out of curiousity: do you think making the constants explicit will be helpful for anything?
For the proof of 9.1 it's totally irrelevant, right?

[Johan Commelin]

Do you think they might be useful in a different direction, at some point?

[Peter Scholze]

I don't know any use of them, but I just think it's worth doing it

[Peter Scholze]

I think one gets a better idea of what's happening in the proof if one has some idea of how large the numbers are

[Johan Commelin]

Peter Scholze said:

some idea of how large the numbers are

answer: astronomical :rofl: :stuck_out_tongue_wink:

[Peter Scholze]

Well, it's not even tower-exponential

[Peter Scholze]

(Still large enough that an ultrafinitist might object to them :wink: )

[Johan Commelin]

Sure, it can always be worse (-; No busy beavers in sight.

[Johan Commelin]

Yeah, the ultrafinitists will probably have to call quits once m > 3?

[Peter Scholze]

Also, getting actual verified constants is much easier after a computer formalization than after a proof on paper (which may have small oversights)

[Kevin Buzzard]

In one of Richard Taylor's early papers about attaching p-adic Galois representations to Hilbert modular forms, he makes a mistake when writing down a pairing on a finite free Z_p-module (there is some duality involved and he misses a scaling factor which is a binomial coefficient). When I was his PhD student going through this paper I spotted this slip, which temporarily breaks a proof, but one can fix it up without too much trouble (the "robustness of mathematics") and the theorems Taylor claims (which don't mention constants explicitly) are all OK without any change at all. I mentioned this to him, and he said "oh golly, so these constants in the intermediate results are out by some power of p, I think some other people might have used those constants to do something else" and then we never talked about it again and it was such a minor issue that I don't think he ever issued a correction.

[Peter Scholze]

By the way, as it's official now: Congratulations on the plenary talk at the ICM 2022!!

[Kevin Buzzard]

Thanks!

[Scott Morrison]

col_exact.lean is broken atm?

[Johan Commelin]

Ooh, is it?

[Johan Commelin]

It seemed to compile for me when I last pushed.

[Johan Commelin]

Let me push something that builds.

[Johan Commelin]

Aahrg, building takes so long these days.

[Johan Commelin]

I guess we should also untangle the import structure of this project a bit.

[Johan Commelin]

@Scott Morrison I pushed

[Scott Morrison]

(I was actually attempting some import minimisation when I noticed col_exact... :-)

[Johan Commelin]

Pushed another sorry-fix

[Scott Morrison]

I pushed an import reduction, and will hopefully have the c0 stuff soonish. :-)

[Johan Commelin]

Merci!

[Johan Commelin]

I was actually surprised to learn that we don't use the constants at all until all the way at the end of the proof.

[Johan Commelin]

I guess we can split thm95/constants.lean into a file that is used by normed_spectral and "the rest".

[Johan Commelin]

That way a change in constants.lean doesn't cause a recompile of normed_spectral and 30% of the project that depends on it.

[Johan Commelin]

Anyway, lunch time here.

[Scott Morrison]

I am so confused.... master compiles fine. I replace a sorry with something that typechecks, and then something somewhere else doesn't typecheck... :-(

[Scott Morrison]

I splits constants.lean, adding constants_2.lean...

[Scott Morrison]

@Johan Commelin earlier today you added BD as an argument to c₀, but I don't understand why. None of the constraints mention BD.

[Scott Morrison]

@Johan Commelin (sorry, I know you're at lunch). I am increasingly worried there is an off-by-one error in an m, that has been hidden by sorries. To reproduce, try moving m and Λ after the colon in the signature of c₀ (but leave the definition as sorry!), then look at the error in default.lean. If you're around later maybe you can help me work out what is broken.

[Johan Commelin]

@Scott Morrison hi, I'm back

[Johan Commelin]

Let's see if we can sort this out.

[Riccardo Brasca]

I've also time to help if you need help
(and I am adding the dual snake lemma to the blueprint)

[Johan Commelin]

I think we got it fixed in a brief video call

[Scott Morrison]

Okay, c₀ is defined, and all its lemmas are proved, no more sorries!

[Scott Morrison]

One proof still should be golfed.

[Johan Commelin]

Awesome!

[Scott Morrison]

And associated for_mathlib PR: #7710.

[David Michael Roberts]

@Scott Morrison do you mean in constants2.lean?

[Scott Morrison]

Yes.

[Scott Morrison]

No!

[Scott Morrison]

Sorry, there are still sorries in constants_2.lean. Just nothing related to c₀.

[Scott Morrison]

This was the easy part of constants.lean that Johan described above. The really tangled one is still available. :-)

[David Michael Roberts]

OK, just checking. It seemed just a tad too good to be true :-)

[David Michael Roberts]

And I'm just a spectator here, so unfortunately I can't join in the fun (and I'm meant to be doing other work tonight anyway).

[Johan Commelin]

Sounds like an excellent opportunity for www.structuredprocrastination.com :stuck_out_tongue_wink:

[Peter Scholze]

Well I like stand and cheer from the sidelines :smile: :grinning_face_with_smiling_eyes: :sunglasses:

[Johan Commelin]

Sorry count these days:

3       src/prop819.lean
2       src/thm95/col_exact.lean
4       src/thm95/constants_2.lean
2       src/prop819/locally_constant.lean
1       src/for_mathlib/Profinite/locally_constant.lean
Total:  12

[Johan Commelin]

Concerning the constants, I think that with the stuff that Patrick did last night, the tangle should be a lot less of a headache now.

[Adam Topaz]

The sorry in for_mathlib/Profinite/locally_constant is in a comment :wink:

[Adam Topaz]

But that's just because I haven't decided on the best formulation yet...

[Adam Topaz]

Same goes for the two sorry's in prop819/locally_constant

[Johan Commelin]

Ooh, my lousy way of counting also counts comments...

[Adam Topaz]

So there are only 3 sorry's left for 8.19, and they're all in src/prop819.lean

[Johan Commelin]

I see... but do you think you will uncomment those others?

[Adam Topaz]

No they won't be uncommented, but the sorry count might increase before it decreases ;)

[Johan Commelin]

Sure!

[Johan Commelin]

In col_exact there already 10 sorry's again by now (-;

[Peter Scholze]

Didn't we start with just one sorry? What have we been doing all this time? :wink:

[Peter Scholze]

Adam, do you still have questions on the best pen and paper proof of something? Or is it just about writing the Lean code?

[Johan Commelin]

I guess we broke that massive concave sorry into many small convex sorrys which are actually approachable (-;

[Adam Topaz]

No, I have a way forward with 8.19. It all boils down to proving that given a cofiltered limit $X = \varprojlim_i X_i$ with $X_i$ profinite, and a clopen set $U$ of $X$, there is some $i$ and some clopen $U_i$ of $X_i$ such that $U$ is the pullback of $U_i$. Of course, this corresponds to the case where the discrete set in question is $\{0,1\}$, but there's a way to upgrade this to the general case without too much trouble.

[Adam Topaz]

And the statement about clopens seems formalizable using the explicit topology on docs#Top.limit_cone and the fact that clopen sets form a basis for the topology of a profinite set, which Patrick has already formalized.

[Peter Scholze]

OK, great!

[Adam Topaz]

I was hoping to just use some categorical shenanigans, but even if you work out everything in terms of Stone duality, it comes down to proving that $C^0(-,2)$ commutes with cofiltered limits, which then reduces to the above statement about clopens

[Peter Scholze]

Actually I did think about Stone duality as well here :wink: but yeah, it doesn't really seem to be of direct help here (even if it would of course be nice to formalize Stone duality)

[Adam Topaz]

I think there was some talk about formalizing Stone duality at some point. It would be a fun project :)

[Scott Morrison]

One question about c_0: I just wrote a recursive definition that exactly matched the shape of the constraints, but it means that it's left unobvious how big c_0 actually is. Is this worth fixing by providing a more explicit bound, or does it not matter?

[Patrick Massot]

The quest for constants is done. It's not yet on master because I haven't fixed all files that depends on this constant defining file. All files that assumed that K₁ depended only on m must now take into account that it also depends on BD c' r r'.

[Patrick Massot]

Note that I haven't prove any upper bound on those constants. That's a job for another day (and I will need some input from the explicit Breen-Deligne construction).

[Johan Commelin]

@Patrick Massot Wonderful! Thanks you so much.

[Johan Commelin]

@Scott Morrison No, the $c_0$ is not really one of the "main" constants. I don't think Peter cares about how it grows. In particular, it doesn't influence the constants that Patrick worked on.

[Johan Commelin]

I merged the branch into master, and fixed whatever broke.

[Johan Commelin]

Sorry count:

3       src/prop819.lean
7       src/thm95/col_exact.lean
2       src/prop819/locally_constant.lean
8       src/for_mathlib/Profinite/clopen_limit.lean
1       src/for_mathlib/Profinite/locally_constant.lean
Total:  21

[Peter Scholze]

Yes, how $c_0$ grows was not part of Question 9.9, although it would be nice to get an idea of what's going on. I think it's pretty tough to figure it out, though, as it depends on the size of the finite generating set in Gordan's lemma, and I don't know how effectively this can be bounded. (I don't know how the formalization is done now, but things like Hahn--Banach or Krein--Milman probably make heavy use of choice in their usual proofs. In the current finite-dimensional situation this is surely overkill, but still.) In any case, not a concern right now.

[Johan Commelin]

I think that Gordan's lemma can in principal be made effective. And the generators of the norm in the polyhedral lattice quotients can also be made effective. (At the moment Lean forgets them as soon as the proof is over.)

[Yaël Dillies]

Krein-Milman indeed uses Zorn's lemma to establish the existence of an extreme point. I agree with Johan on Gordan's lemma.

[Yaël Dillies]

Actually, if you're working over finite dimensional stuff, Carathéodory-Minkowski is a much better choice. It should actually be pretty easy for me to prove it given that Carathéodory is already in mathlib.

[Peter Scholze]

(The reason I don't care about $c_0$ so much is the following. In the end, you prove that for $c\geq c_0$, some transition map $H^m(C_{kc}^\bullet)\to H^m(C_c^\bullet)$ is zero. We can already estimate $k$ in terms of $m$, and it will likely be something enormous like $3^{3^{m^2}}$. So $C_{kc}$ will definitely involve an index $kc\geq kc_0\geq k$ that is astronomical. The question of how large $c_0$ is is then probably secondary -- it will probably at most be of roughly the same size as $k$. By the way, in my analogy with buses, trains, and airplanes, the indices like $kc$ roughly correspond to the required number of airports/train stations/bus stations ;-).)

[Stanislas Polu]

Adam Topaz said:

Can we set gptf loose on that file for three weeks and see what happens?

Can you point me to the files/statements of interest, I can setup an experiment to test this out! Thanks!

[Stanislas Polu]

(If there is any left to work on obviously)

[Johan Commelin]

@Stanislas Polu There are no sorry's left, but it could of course still be fun to see what gptf makes of these files.

[Johan Commelin]

The files in question are in src/thm95/constants/

[Stanislas Polu]

Cool will look into it!