laurent measures

Stream: condensed mathematics

[Johan Commelin]

I'm doing a pretty large review/refactor/golf of stuff in laurent_measures/. More simp-lemmas. Definition of multiplication by T and T⁻¹.

[Johan Commelin]

I just pushed.

commit f1441231bde1980b6073e43339780eda3cffa7a4 (HEAD -> master, origin/master, origin/HEAD)
Author: Johan Commelin <johan@commelin.net>
Date:   Fri Feb 4 18:50:34 2022 +0000

    review laurent measures

 src/laurent_measures/basic.lean   | 647 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-----------------------------------------------------------------------------------------
 src/laurent_measures/bounded.lean |  73 ++++++++-------------
 src/laurent_measures/theta.lean   |  13 ++--
 src/laurent_measures/thm69.lean   |  79 +++++++----------------
 4 files changed, 395 insertions(+), 417 deletions(-)

[Johan Commelin]

@Filippo A. E. Nuccio This somewhat impacts your files. I could golf the definition of ϕ to a 1-liner because we now have shift k which is multiplication by T^k.

[Filippo A. E. Nuccio]

OK, I see.

[Filippo A. E. Nuccio]

I am now working on aux_lemmas.lean which does not seem impacted, right?

[Filippo A. E. Nuccio]

thm69.lean was actually sorry-free (although one lemma remains to be proved in aux_lemmas, so Theorem 6.9 by itself was not yet sorry-free).

[Johan Commelin]

Aah, it somehow seemed to be broken

[Johan Commelin]

I will see what's wrong.

[Filippo A. E. Nuccio]

It was not compiling? I had no errors locally.

[Johan Commelin]

@summable_smaller_radius _ _ F.d (F.summable s) (lt_d_eq_zero _ _) r_half shows up a lot... seems like a good thing to extract into a lemma.

[Johan Commelin]

I found out my mistake. You had lemmas in the aux file but also commented out versions in the other file.

[Johan Commelin]

And so I somehow got confused about what I was doing, and ended up fixing the wrong lemma :oops: :see_no_evil:

[Filippo A. E. Nuccio]

I apologise, I did not think you would be working on this and code was not very clean.

[Filippo A. E. Nuccio]

Concerning @summable_smaller_radius... it is a lemma, you are saying that it calls too many varialbes, right?

[Filippo A. E. Nuccio]

And that it was poorly created, because I actually call it with a @.

[Filippo A. E. Nuccio]

My strategy now was to try to rush ASAP to having Theorem 6.9 completely sorry-free, and then to improve my code.

[Johan Commelin]

Filippo A. E. Nuccio said:

Concerning @summable_smaller_radius... it is a lemma, you are saying that it calls too many varialbes, right?

Yeah, I think you could have a special case that hard codes the F.summable s and r_half inputs, etc...

[Filippo A. E. Nuccio]

OK, how do you prefer to advance? I certainly agree with your remark (and was not satisfied about the API).

[Johan Commelin]

Let me first fix the stuff I broke

[Johan Commelin]

I'm almost done.

[Johan Commelin]

After that, we can golf more (-;

[Filippo A. E. Nuccio]

No problem, I am on aux_lemmas right now.

[Johan Commelin]

pushed

[Filippo A. E. Nuccio]

I have pulled, but it is a bit slow. Do you still have sorrys in thm69?

[Johan Commelin]

Nope, it's sorry-free again

[Filippo A. E. Nuccio]

Ok, great, thanks. I am certainly aware that things need to be golfed, but I am somewhat in the middle of finishing the proof and I will do this later, if you agree.

[Johan Commelin]

Sure, totally fine

[Johan Commelin]

I've started on the SES

$$0 → ℤ[T⁻¹] → ℒ_{r'}(S) → \bar{ℳ}_{r'}(S) → 0$$

[Johan Commelin]

See Mbar/ses.lean for a couple of sorries.

[Filippo A. E. Nuccio]

It is a ses of what?

[Johan Commelin]

ProFiltPseuNormGrpWithTinv₁ r'

[Filippo A. E. Nuccio]

I am done for tonight, time for dinner. Again, the code is a bit of a mess, but it will be improved!

[Filippo A. E. Nuccio]

At least, it compiles.

[Johan Commelin]

Ok! Enjoy your evening

[Johan Commelin]

Johan Commelin said:

See Mbar/ses.lean for a couple of sorries.

This is now sorry-free again.

[Filippo A. E. Nuccio]

The proof of Theorem 6.9 is now entirely sorry-free.

[Filippo A. E. Nuccio]

I still need to :golf: it, and of course
(i) It is only for finite S, for the time being.
(ii) It is only a "naive" SES checked on elements, not in the right category.

[Johan Commelin]

Amazing! Huge congrats!

[Johan Commelin]

In my LTE post this morning, I said that the BD-lemma is the only big milestone left. And I had this little voice nagging me, saying "But 6.9 isn't completely done yet!". I just replied to that voice "I'm sure Filippo will have it done in 2 or 3 days". Bingo!

[Filippo A. E. Nuccio]

Great! BTW, I am now going to read through all your post.

[Adam Topaz]

This is great @Filippo A. E. Nuccio ! Do we know that these map $\theta$ and $\psi$ are morphisms in ProFilt..._1? I suppose that the fact that they're additive homomorphisms should be easy, while continuity would be the most challenging thing to prove. Once we know that, we could use something similar to how Lemma 9.8 is formalized in the profinite case to obtain the profinite case of 6.9.

[Filippo A. E. Nuccio]

No, exactly, we do not know this yet. This is precisely my next goal.

[Filippo A. E. Nuccio]

I already have a blurry proof of additivity, but I am now going to upgrade them to morphisms in the right category.

[Filippo A. E. Nuccio]

It will take a little bit, but I am not too scared.

[Filippo A. E. Nuccio]

@Johan Commelin I guess that the right place to do this will be in Mbar/ses.lean, where you have written down the ses, right?

[Adam Topaz]

That ses is the one for Mbar. Theorem 6.9 is the other one, right?

[Filippo A. E. Nuccio]

Oh right!

[Adam Topaz]

I think we should add a laurent_measures/ses.lean ;)

[Filippo A. E. Nuccio]

OK!

[Johan Commelin]

Note that

def ϕ : ℒ S → ℒ S :=
λ F, 2 • shift (-1) F - F

should make it easy to prove that this is a non-strict morphism.

[Johan Commelin]

Because shift (-1) is a morphism. So it is 2 • some_morphism - id.

[Filippo A. E. Nuccio]

Oh great, thanks.

[Filippo A. E. Nuccio]

I am starting with laurent_measures/ses.lean and I will write some of the needed lemmas. I will try to immediately implement your suggestion, or at least copying it as a comment for later use.

[Johan Commelin]

Proving continuity of θ will be more work, I guess.

[Filippo A. E. Nuccio]

We'll see along the way, I guess.

[Filippo A. E. Nuccio]

I see that in thm69.lean we now have a variables [fact (0 < r)] as well as a lemma r_pos : 0 < r :=.... Do we really need the former, given the latter? I understand that as it is it cannot be found by type inference, but can't we use the lemma in some way? Otherwise it seems to me that we are adding as assumption something that we can prove, no?

[Adam Topaz]

You could declare it as instance : fact (0 < r) := ... I suppose fact ... is needed for shift?

[Filippo A. E. Nuccio]

Yes, indeed. I wanted to declare it as an instance, but I want to check if it is a good idea.

[Johan Commelin]

Yeah, instance is the way to go

[Johan Commelin]

Johan Commelin said:

Because shift (-1) is a morphism. So it is 2 • some_morphism - id.

@Filippo A. E. Nuccio ooh, probably this morphism isn't even strict... so we'll need a bit more glue.

[Filippo A. E. Nuccio]

I would suggest that I start implementing the API and then we'll see where the difficulties lie.

[Johan Commelin]

@Filippo A. E. Nuccio Yes. Just for the record, comphaus_filtered_pseudo_normed_group_with_Tinv_hom would be the non-strict version.

[Johan Commelin]

I am contemplating a global search-replace that does s/pseudo_normed_group/png/ in all these names.

[Johan Commelin]

They are way too long.

[Filippo A. E. Nuccio]

Well, they are long but it is clear what they mean... p_nrm_grp?

[Adam Topaz]

:+1: from me for changing all instances of pseudo_normed_group to png and PseuNormGrp to PNG.

[Adam Topaz]

Maybe also profinitely_filtererd to pf, ProFilt to PF, comphaus_filtered to chf, CompHausFilt to CHF, {with_Tinv,WithTinv} to T

[Peter Scholze]

Ah, I detest abbreviations :upside_down:

[Peter Scholze]

(I'm not formalizing, so don't listen to me)

[Johan Commelin]

But comphaus_filtered_pseudo_normed_group_with_Tinv_hom is really long...

[Adam Topaz]

Peter Scholze said:

Ah, I detest abbreviations :upside_down:

I usually agree, but...

Johan Commelin said:

But comphaus_filtered_pseudo_normed_group_with_Tinv_hom is really long...

[Adam Topaz]

I'm about to write down profinitely_filtered_pseudo_normed_group_with_Tinv.to_comphaus_filtered_pseudo_normed_group_with_Tinv and just that alone is longer than 100 chars which is our "standard" limit for line length.

[Filippo A. E. Nuccio]

I also detest abbreviations a little bit, I would propose something in between. We can look for "speaking abbreviations", like grp for group, or filt for filtered, pro for profinitely. But pfg for profinitely filtered group looks a bit too succint to me.

[Adam Topaz]

Well, it would be pfpng

[Filippo A. E. Nuccio]

That could also be a potentially finite pro-nilpotent gauge, no?

[Johan Commelin]

Also, we can have docstrings that spell out the full thing

[Filippo A. E. Nuccio]

Johan Commelin said:

Also, we can have docstrings that spell out the full thing

True, but are we committed to a very strict discipline on writing docstrings?

[Johan Commelin]

No, but we can certainly do it for these definitions.

[Filippo A. E. Nuccio]

Ok, I don't want to insist too much. I am just a bit scared that we insert some Qabbalah where there is none (and there is already plenty of it).

[Filippo A. E. Nuccio]

Another option would be to come up with a short (and nice?) name for the final category where we are going to work (I guess it is CompHausPseudoNormedGroupwithInvT) and to keep all the rest quite long, considering it as "working mess" rather than something that will be often read.

[Adam Topaz]

I just added CompHausFiltPseuNormGroupWithTinv (this was not as easy as one would have expected...).
The strict version of that category is still missing, but I need to do other things for a little while. If anyone wants to add the strict version, that would be helpful (the functors between these should also be added)

[Filippo A. E. Nuccio]

OK, I will see if I can do something - at any rate I will need to get acquainted with all this to upgrade the actual version of 6.9 to a true ses.

[Kevin Buzzard]

Can't we do this with abbreviations? I am hooked on the long names.

[Johan Commelin]

Ok ok, we don't need to rush the renaming.

[Johan Commelin]

But people have written LRS instead of LocallyRingedSpace for decades, probably because they wanted to save ink :wink:

[Filippo A. E. Nuccio]

I am fighting a bit against the fact that (filtration (ℒ ϖ) c) and { F : (ℒ ϖ) | ∥ F ∥₊ ≤ c} do not seem to be identical, although they are the same subsets of (ℒ ϖ): what I mean is that their coercions to Type are not the same type. So, if I define

def U (F : filtration (ℒ ϖ) c) (B : ℤ) : set (filtration (ℒ ϖ) c) := λ G, ∀ s n, n < B → F s n = G s n

and

def V (F : filtration (ℒ ϖ) c) (B : ℤ) : set ({ F : (ℒ ϖ) | ∥ F ∥₊ ≤ c}) :=
  λ G, ∀ s n, n < B → F s n = G s n

then I cannot say that U F B = V F B (I can get some U F B == V F B, with heq instead of eq). This is already a bit strange, since the fact that the second definition is accepted seems to show that Lean undestand that they are (definitionally) equal. The problem is that the first definition is very useful for everything done so far and the second is the one directly connected to the definition of the topology, so proving V is open is OK, but I need this for U. I think this is related to the fact that the following foo does not type-check

noncomputable theory
lemma foo (α : Type) (s t : set α) (s₁ : set s) (t₁ : set t) (H : s = t) (hs : s₁ = set.univ)
  (ht : t₁ = set.univ): s₁ = t₁ :=

whereas the following bar (with == instead of =) type-checks.

noncomputable theory
lemma bar (α : Type) (s t : set α) (s₁ : set s) (t₁ : set t) (H : s = t) (hs : s₁ = set.univ)
  (ht : t₁ = set.univ): s₁ == t₁ :=

Any idea?

[Adam Topaz]

@Filippo A. E. Nuccio Are these Laurent measures on a profinite set $S$?

[Filippo A. E. Nuccio]

On the singleton.

[Adam Topaz]

Ah

[Adam Topaz]

Can you point me to where this is defined?

[Filippo A. E. Nuccio]

This what? U and V?

[Adam Topaz]

filtration (ℒ ϖ) c

[Adam Topaz]

I..e. where is (ℒ ϖ) defined?

[Adam Topaz]

Nevermind I found it

[Adam Topaz]

These seem to work for me...

example : filtration (ℒ ϖ) c = { F | ∥ F ∥₊ ≤ c } := rfl
example : (filtration (ℒ ϖ) c : Type*) = { F | ∥ F ∥₊ ≤ c } := rfl

[Filippo A. E. Nuccio]

But if you have V : set (filtration (ℒ ϖ) c) and U : set ({ F | ∥ F ∥₊ ≤ c }), can you state U = V? They are of different types.

[Adam Topaz]

This also works:

def U (F : filtration (ℒ ϖ) c) (B : ℤ) : set (filtration (ℒ ϖ) c) := λ G, ∀ s n, n < B → F s n = G s n
def V (F : filtration (ℒ ϖ) c) (B : ℤ) : set ({ F : (ℒ ϖ) | ∥ F ∥₊ ≤ c}) :=
  λ G, ∀ s n, n < B → F s n = G s n

example : U = V := rfl

[Filippo A. E. Nuccio]

Ah ops

[Filippo A. E. Nuccio]

:thinking: OK, something must be weird on my side. Thanks for checking, I will see what I have wrong here.

[Adam Topaz]

Note that filtration (ℒ ϖ) c and { F | ∥ F ∥₊ ≤ c } are actually defeq, so their associated types are also defeq

[Filippo A. E. Nuccio]

Yes, this is what I thought initially. But indeed by copy-pasting your code, my Lean complains.

[Adam Topaz]

In the code you posted here

noncomputable theory
lemma foo (α : Type) (s t : set α) (s₁ : set s) (t₁ : set t) (H : s = t) (hs : s₁ = set.univ)
  (ht : t₁ = set.univ): s₁ = t₁ :=

the two sets s and t are only propositionally equal, which is why you had to use heq for your lemma bar..

[Adam Topaz]

Hmm... I'm 36 commits behind. let me pull and try again

[Filippo A. E. Nuccio]

No, I don't think this would make any difference.

[Filippo A. E. Nuccio]

I am also a bit behind on my branch.

[Filippo A. E. Nuccio]

Let me check on master.

[Filippo A. E. Nuccio]

@Adam Topaz I am having some troubles compiling and I almost need to go to dinner, so I will check again tomorrow morning. If this compiles on your side, it will on my as well, eventually, which is precisely what I was hoping for to adapt my proof of the openness of V to that of U. Thanks for the help, I will post here tomorrow if everything went well.

[Adam Topaz]

I'm on the latest commit on master, and it seems to work fine for me....

[Filippo A. E. Nuccio]

OK, following @Adam Topaz ' proof of is_open_U, I closed the last sorry and laurent_measures/ses.leanis now sorry-free (and pushed).

[Johan Commelin]

That's a milestone! Really great!

[Kevin Buzzard]

I've been distracted by developing a theory of binary sequences as part of a more conceptual proof of 7.2 but I'll get there in the end, and then ses2 will also be sorry-free