Task 52

Stream: Carleson

[Joachim Breitner]

Quick question about task 52:

that if the subset has no chains of length n+1 then the union of the first n sets is the original set

What is the general notion for “chain of length n” and “has no chain of length n”?
Given a partial order and two elements x and y , what is the idiomatic way to say that x < … (n steps) < y

[Yaël Dillies]

There's no idiomatic way. I'd say use a list [x] ++ l ++ [y] and assume it is sorted

[Kevin Buzzard]

I thought that we had all this chain and krull dimension stuff now? (On mobile but search for krull dimension maybe?)

[Joachim Breitner]

Indeed there is krullDim (α : Type u_1) → [inst : Preorder α] → WithBot (WithTop ℕ), which may be suitable here

[Kevin Buzzard]

So maybe docs#LTSeries is what you're looking for?

[Kevin Buzzard]

Oh I see, but this doesn't have fixed endpoints

[Joachim Breitner]

Maybe I am simply looking for some form of relation iteration, possibly R^n

[Joachim Breitner]

I tried a few things in https://github.com/fpvandoorn/carleson/pull/90, still very early.

My main question is the interface to

/-- Part of Lemma 5.5.2 -/
lemma iUnion_L0' : ⋃ (l ≤ n), 𝔏₀' (X := X) k n l = 𝔏₀ k n :=

The generalization of that lemma needs this extra assumption “subset has no chains of length n+1”, and I wonder if you already know in which form that assumption is most convenient? the krulllDim sounds right, but maybe be awkward (WithBot and WithTop complications, supremums etc.). Maybe

  (hlength : (xs : LTSeries s) → xs.length ≤ n)

is easiest?

Although it feels very natural to identify 𝔏₀' k n l with those elements in 𝔏₀ k n that have height l (in that set), and mathlib’s height definition goes via krulllDim. And lacks lots of API, it seems.

[Joachim Breitner]

(And it’s dangerous to start something like this two hours before bedtime, because then bedtime loses… :-D)

[Kevin Buzzard]

@Fangming Li (John) this is a use case for DimensionLT perhaps

[Joachim Breitner]

After thinking about it a bit, I think

  (hlength : (xs : LTSeries s) → xs.length ≤ n)

is a naturally basic way to express this, in particular as the strict bound isn’t needed. The lemma to get there would be something along the lines

lemma exists_ltseries_of_mem_foo {n : ℕ} {x : α} (hx : x ∈ by_height s n) :
  ∃ xs, xs.length = n /\ ∀ i. (xs i) ∈ by_height s i

from which the existing

lemma exists_le_of_mem_𝔏₁ {k n j l : ℕ} {p : 𝔓 X} (hp : p ∈ 𝔏₁ k n j l) :
    ∃ p' ∈ ℭ₁ k n j, p' ≤ p ∧ 𝔰 p' + l ≤ 𝔰 p := by

should follow, together with StrictMono 𝔰.

If this by_height construction goes towards mathlib, then something like

lemma mem_foo_iff_height {n : ℕ} {x : s} :
  x.val ∈ foo s n ↔ height s x = n := by

would be a nice addition, but maybe not strictly necessary for Task 52.

[Floris van Doorn]

The last lemma might not be strictly necessary for the task, but if it goes into Mathlib, it is nice to have!

[Joachim Breitner]

More thoughts:
This minLayer really is just the partition of the set by the height of elements. So I'd say I'd complete the (almost non-existent) API for height, and hopefully we'll get the lemmas we need from that easily:

• An element of finite height n has a LTSeries ending in it of length n
• Every series of length n ending in the element has at position I an element of height I
• A series of length n ends in an element of height at least n
• For an element of height n there exists a series of length n ending in it (this is almost all that's needed for the lemma that gives you a p' with s differing by at least n , and maybe allows to strengthen it to unblock Jeremy)
• The elements of height n are the minimal elements when removing elements of height <n. This lemma proves the recursive equation in the blueprint.

Let's see how many international flights this takes :-)

[Joachim Breitner]

Oh, there is docs#Set.subchain in Mathlib.Order.Heightwhich already has plenty of lemmas, all phrased in terms of List.Chain' rather than docs#LTSeries. I guess LTSeries is a bit nicer here, mostly becaue it's no-empty.

[Joachim Breitner]

Ok, pushed some reasonable preliminary version to https://github.com/fpvandoorn/carleson/pull/90
It contains some reasonable API coverage for height, defined as

noncomputable def height {α : Type*} [Preorder α] (a : α) : ℕ∞ :=
  ⨆ (p : {p : LTSeries α // p.last = a}), p.1.length

(which I believe can replace the height definition in mathlib).

Based on that there is also a definition

Set.with_height.{u_1} {α : Type u_1} [Preorder α] (s : Set α) (n : ℕ) : Set α

that is the minLayer in Jeremy’s PR. It can equivalently be defined using the recursion as in the repo right now, or via

lemma Set.mem_with_height_iff (s : Set α) (n : Nat) (x : α) :
    x ∈ s.with_height n ↔ ∃ (hx : x ∈ s), height (⟨x, hx⟩ : s) = n := by

This is then used to fill in the blanks in DiscreteCarleson.

Maybe of particular interest is my proof for

lemma exists_le_of_mem_𝔏₁ {k n j l : ℕ} {p : 𝔓 X} (hp : p ∈ 𝔏₁ k n j l) :
    ∃ p' ∈ ℭ₁ k n j, p' ≤ p ∧ 𝔰 p' + l ≤ 𝔰 p := by

Which goes like this

• From hp : p ∈ 𝔏₁ k n j l we know that p has height l
• Therefore we have a sequence p' < … < p of length l
• 𝔰 is strictly monotone, so 𝔰 p' < … < 𝔰 p is still a sequence of length l
• That’s a sequence in Z, so 𝔰 p' + l ≤ 𝔰 p follows.

Possibly that sequence p' < … < p is actually of interest beyond that lemma?

[Joachim Breitner]

Questions as of now:

• Is the API provided by ToMathlib.Height roughly ok?
• What's a better name for Set.with_height?
• Worth merging soon to get the API in to be able to build on it, or should I finish the few remaining sorries (some results about infinite height elements) and do general cleanup first?
• Assuming the height definition is mathlib-worthy, is it a good idea to upstream in parallel to the project, or less friction to upstream once it’s done and stable? (I think the Set.with_height is a bid too specific to upstream.)

[Joachim Breitner]

Nice task by the way :-)

[Yury G. Kudryashov]

Note that we have docs#height and docs#krullDim in Mathlib, and AFAIR they are (were?) off by 1.

[Yury G. Kudryashov]

I think that these 2 definitions should be deduplicated. I hope that you aren't going to add another one instead.

[Yury G. Kudryashov]

I think the Set.with_height is a bid too specific to upstream

I hope that the whole project will be upstreamed one day, because I think that we want to have the main result[^1] in Mathlib.

[^1]: More precisely, I'm sure that we want the more classical result in Mathlib, but if we'll have a more precise result formalized, then why not add it instead?

[Joachim Breitner]

Yury G. Kudryashov said:

Note that we have docs#height and docs#krullDim in Mathlib, and AFAIR they are (were?) off by 1.

I know about docs#height; my proposal is to replace that with my definition (it’s very similar, but mathlib’s has a WithBot around the result type which mine doesn’t). docs#height doesn’t have much of an API or uses yet anyways, so I hope this won’t be disruptive.

I hope that the whole project will be upstreamed one day, because I think that we want to have the main result[^1] in Mathlib.

Good point. Well, s.with_height n (or maybe better called Set.by_height?) isn’t inherently bad. I am just wondering if it’s needed when it’s mostly just the preimage of n under height in the partial order restricted to a set s. But maybe that’s already enough to justify its own definition.

[Joachim Breitner]

This is now sorry-free up to #Is there code for X? > ENat.iSup_eq_coe_iff

[Floris van Doorn]

I think all of this (including with_height is Mathlib-worthy. I think your definition is better than height in Mathlib (which should really be namespaced). Mathlib's height a can never be \bot, right?

I am not sure about upstreaming the whole project, but that is a separate discussion (which I'm certainly happy to have!)

[Joachim Breitner]

Floris van Doorn said:

I think all of this (including with_height is Mathlib-worthy. I think your definition is better than height in Mathlib (which should really be namespaced). Mathlib's height a can never be \bot, right?

Exactly!

So what is the preferred course of action? How about we merge this quickly to be able to build on build on it within carleson. Then I start upstreaming to mathlib, cleaning up in the mathlib PRs based on maintainer reviews, and removing bits from carleson as they appear in the mathlib we follow there?
(If we upstream it anways, and assuming that the mathlib review process will have more clean-up inputs, it seems to be more efficient to do most cleanup on the way to mathlib, rather than first in the carleson and then again, based on more feedback, on the way to mathlib.

[Floris van Doorn]

Yes, I would definitely like to have this available in carleson soon, so merging it to carleson quickly and then making PRs to mathlib sounds perfect!

[Yury G. Kudryashov]

Mathlib used to have a different definition of height, then I complained about 2 almost identical definitions (height and krullDimension) and someone deduplicated them. I remember that they were off by one.

[Yury G. Kudryashov]

OMG, we still have docs#height and docs#Set.chainHeight

[Yury G. Kudryashov]

It would be nice to clean up this mess.

[Yury G. Kudryashov]

See #mathlib4 > RelSeries vs List.chain vs Order.height

[Joachim Breitner]

The height is off by one against the math literature, but on the other hand it's natural to those who like start counting at 0, and it's a but strange to map to the Natural numbers but don't use the zero.

What is the convention in mathlib? Stick to the literature, or be at liberty if something is off by one of it leads to a more natural definition?

[Kevin Buzzard]

I'm not clear about "the math literature" in general, but certainly in algebraic geometry/commutative algebra the ring $\R[X,Y,Z]$ has got Krull dimension 3 because a maximal chain of prime ideals is $0\subset(X)\subset(X,Y)\subset(X,Y,Z)$, that being a chain of length 3 -- with four prime ideals in it. The prime ideal $(X)$ has got height 1 and the prime ideal $0$ has got height 0. We certainly need to stick to these conventions in commutative algebra or we'll confuse everyone doing commutative algebra and algebraic geometry. If there are other conventions in other parts of mathematics (are there?) then we might have to namespace different concepts of height and document them well.

[Joachim Breitner]

Oh, ok, but that's the height I'm currently calculating - minimal elements have height 0.

[Yury G. Kudryashov]

Set.chainHeight is off by one. I think that it should be fixed, and possibly merged with height (which should take values in ENat). Also, Krull dimension should take values in WithBot ENat (defeq to WithBot (WithTop Nat) but we have lemmas about ENat).

[Floris van Doorn]

I was already thinking that it might be nice to have height take a Set argument (since that is nicer than taking the height of a subtype). In that case it might be even easier to remove chainHeight.

[Joachim Breitner]

It seems that there is always a tension between phrasing something in terms of sets or types? Certainly when defining it using a type is easier, and especially since (so far) there is always one set, I chose to define height without the additional restriction. My inclination is to keep it that way, and if you need the set-restriction use Set.withHeight or use the subtype, and maybe we can extend the API to make that more usable.

But I don't have much experience with that aspect of API design, so maybe doing it all with sets is actually better. But it seems that then we'd also want a set-restricted version of or LTSeries?

[Floris van Doorn]

Yet, a set-restricted version of LTSeries also seems good to me: it often shows up, and then you don't have to move to subtypes, which is often a bit annoying.

[Yury G. Kudryashov]

BTW, is it really more convenient to work with Lists rather than Chains?

[Yury G. Kudryashov]

Yury G. Kudryashov said:

BTW, why not use something like this?

def myHeight (s : Set α) : ENat := ⨆ (t ⊆ s) (ht : IsChain (⋅ < ⋅) t), Set.encard t

I mean this.

[Joachim Breitner]

Note to myself: the lemmas in https://github.com/leanprover-community/mathlib4/pull/15271/files might allow me to define height more elegantly as a nested inf rather than an inf over a product. Will try once near a computer again

[Kevin Buzzard]

By the way, if you don't want to be dealing with WithBot (WithTop Nat) then note that the same information is captured by the predicates HeightLT n with n a natural.

[Joachim Breitner]

Brief update: I started fleshing out a nice module for height (and soon krullDim) with an API beyond what's needed for Carleson, and hope to PR that to mathlib in a few days or so. Hope I'm not accidentally duplicating someone else's work

[Joachim Breitner]

Getting closer; just opened the draft PR at https://github.com/leanprover-community/mathlib4/pull/15524, but there is more cleanup and docstrings etc. to be done before it’s ready for review. Also, the whole height API ought to be be duplicated for coheight. I hope that clever tricks with defeq or a nice set of duality-simp rules will make this only repetitive.

[Joachim Breitner]

Status update: The PR has now all the definitions and theorems I was planning to add, and everything that isn’t going into that file is in a separate PR:

• feat(RelSeries): {head,last}_map #15387
• feat(RelSeries): eraseLast_last_rel_last #15386
• feat(RelSeries): head_singleton, last_singleton #15384
• feat(LTSeries): toFun_add_sub_le_toFun_{int,nat} #15383
• feat(ENat): isup_add #15344
• feat(RelSeries): LTSeries.iota #15555
• feat(RelSeries): {last,head}_reverse #15556
• feat(RelSeries): RelSeries.take and RelSeries.drop #15557
• feat(ENat): CompleteLinearOrder (WithBot ENat) #15558
• refactor(ConditionallyCompleteLattice): adhere to csSup vs. sSup naming convention #15560

Docstrings and module header not complete yet, but maybe I’ll wait for the dependencies to go through first, in case some of them require non-trivial changes.

[Jeremy Tan]

Why don't you consolidate your PRs? Some of them are just 10 lines or so long

[Joachim Breitner]

You mean after I spent time to nicely separate them into easily reviewable, separate PRs, some of them hopefully correctly labeled easy? :-)

Ok, the two three adding head/tail lemmas to RelSeries functions could be one. I think in that case one was already underway when the need for the next one arose. But they are all easy, so hopefully not much difference either way.

[Kevin Buzzard]

@Jeremy Tan why don't you review some of the PRs, and then you'll see how much easier it is to review a small one!

[Jeremy Tan]

Kevin Buzzard said:

Jeremy Tan why don't you review some of the PRs, and then you'll see how much easier it is to review a small one!

I would consider a PR with 100 total changed lines small

[Yaël Dillies]

I agree Joachim's definitions are possibly a bit too atomic (I would have personally put all the RelSeries lemmas in one PR), but it's definitely better to have too small PRs than two big ones

[Joachim Breitner]

Yeah, for {head,last} it would have definitely be better to have a “I went through all definitions in the module and added the missing lemmas” PR. Would have created this now that I have a few minutes, but two of those PRs have just been merged :)

Adding iota and take/drop in separate PRs is maybe borderline useful as a separation. :shrug:.

[Yury G. Kudryashov]

Could you please add t-order label to all/most of these PRs?

[Joachim Breitner]

Will do!

[Damiano Testa]

Yury G. Kudryashov said:

Could you please add t-order label to all/most of these PRs?

Would it make sense to automatically label PRs with t-<root_folder> for each root folder containing modifications?

[Rida Hamadani]

Damiano Testa said:

Would it make sense to automatically label PRs with t-<root_folder> for each root folder containing modifications?

This leads to the question, if we are formalizing a combinatorics theorem which required us to add a small helper function in the algebra folder, should we add t-algebra in addition to the t-combinatorics?

[Yury G. Kudryashov]

Usually, no.

[Damiano Testa]

I think that, if this is a desirable feature, then we can investigate what to do in such cases, whether the bot should add a single or multiple labels and what heuristics it should use. I just wanted to see if some form of automatic labeling was potentially useful.

[Damiano Testa]

E.g. a simple test would be: if there is a single root folder modified, use that, otherwise do nothing.

[Yaël Dillies]

Damiano Testa said:

Yury G. Kudryashov said:

Could you please add t-order label to all/most of these PRs?

Would it make sense to automatically label PRs with t-<root_folder> for each root folder containing modifications?

t-logic would like to disagree

[Joachim Breitner]

The list of depending PRs is getting smaller, so maybe time to get https://github.com/leanprover-community/mathlib4/pull/15524 itself into shape.

@Floris van Doorn , you mentioned that height should be namespaced. What namespace should I use? Simply namesapce Order? And should krullDim (which is less generic than height) also go into that same namesapce?

[Yaël Dillies]

I think Order.height is a good name

[Johan Commelin]

Is krullDim less generic across the board? In that case it could maybe just be removed? After all, mathlib doesn't have vectorSpace, so why should it have krullDim?

[Joachim Breitner]

Sorry, I meant the name is less generic than height, so the need to namespace height may not apply to krullDim. As mathematical concept’s, they are incomparable (one is for elements, the other one for types), and unless I am missing something both are useful.

[Jeremy Tan]

@Floris van Doorn has been missing from this project for a week now

[Jeremy Tan]

I've just bumped the project to 4.11.0-rc2 at https://github.com/fpvandoorn/carleson/pull/109

[Patrick Massot]

Jeremy Tan said:

Floris van Doorn has been missing from this project for a week now

He may be on vacations. Such things are common at this time of the year.

[Floris van Doorn]

I was indeed on a break, and will not always be online for the next ~month. Expect some periods of time where I will be away for a week or so.
Thanks for doing this very big bump!

[Joachim Breitner]

Status update: The last “tricky” dependency is in (topology on ENat), and the height PR #15524 now only waits on LTSeries.iota (#15555) before the blocked-by-other-PR label disappears and the PR shows upon the review queue

[Kevin Buzzard]

Johan Commelin said:

Is krullDim less generic across the board? In that case it could maybe just be removed? After all, mathlib doesn't have vectorSpace, so why should it have krullDim?

Mathlib did have vector_space back in the Lean 3 days, it was only removed because we couldn't get it to work well with module in Lean 3. I think mathlib should have VectorSpace k V and the fact that we don't might just be a historical accident.

[Joachim Breitner]

The height refactoring PR (#15524) is now dependency-free

[Yaël Dillies]

This is quite huge still. Is there really nothing more you can split off?

[Joachim Breitner]

Hmm, let me page it back in, it’s been a while…

Every second lemma is about coheight. I could move the introduction of coheight into a follow-up PR… ah, but there is already a coheight definitions there, so that makes that awkward.

The last 100lines or so are calculations for concrete orders; these can easily be moved into a separate PR (or even many small ones). Not sure how much that helps.

Or maybe I trim the PR to just the the parts needed to replace the existing definitions, and then one or more (or many) PRs that add new theorems.

None of that really reduces the number of lines to look at, though :shrug:

[Yaël Dillies]

Even if it doesn't really the number of lines, it certainly reduces the cognitive load!

[Joachim Breitner]

Yeah, I see that. I'll see what I can do.

[Joachim Breitner]

Ok, +100loc, that may be a bit better: https://github.com/leanprover-community/mathlib4/pull/16480. Thanks to #show_unused it was not too bad to trim this to the old API

[Yaël Dillies]

Wow yes! Let me move over the comments I started writing

[Joachim Breitner]

Ah sorry for criss-crossing

[Yaël Dillies]

No worries. :smiley:

[Joachim Breitner]

Thanks Yaël for the low-latency review of the first PR! Next batch up at https://github.com/leanprover-community/mathlib4/pull/16500

[Joachim Breitner]

Thanks Yaël again! Next batch up at https://github.com/leanprover-community/mathlib4/pull/16555. I keep hitting nice numbers. (Or maybe most numbers are nice.)

[Yaël Dillies]

I wanted to link to the "smallest uninteresting number" xkcd but apparently I dreamt it up :thinking:

[Joachim Breitner]

Hmm, I know what you mean, but not sure if it was xkcd

[Michael Rothgang]

There is wikipedia for sure

[Jeremy Tan]

Floris van Doorn said:

I was indeed on a break, and will not always be online for the next ~month.

hmm, it's been about a month now

[Joachim Breitner]

JFTR, in case someone looks at this thread:
#16555 is now waiting on @Yaël Dillies ’s #15344 (which was ready, but got a merge conflict three days ago, which I hope I just fixed).

[Joachim Breitner]

Thanks to @Yaël Dillies’s tireless reviewing the 28 PRs split off #15524 are now in, and we can conclude this upstreaming with #15524 itself (which is mostly just the module doc string).

[Yaël Dillies]

28?!? :flushed:

[Joachim Breitner]

• [x] #15421
• [x] #15385
• [x] #15347
• [x] #15345
• [x] #15342
• [x] #15341
• [x] #15196
• [x] #15387
• [x] #15386
• [x] #15384
• [x] #15344
• [x] #15555
• [x] #15556
• [x] #15557
• [x] #15558
• [x] #15601
• [x] #16480
• [x] #16500
• [x] #16555
• [x] #19003
• [x] #19028
• [x] #19110
• [x] #19111
• [x] #19147
• [x] #19148
• [x] #19155
• [x] #19210
• [x] #19251

[Joachim Breitner]

And the branch of #15524 accumulated 204 commits (although that’s an inflated number, due to lots of merge commits and duplications due to squash-merging the dependent PRs)

[Joachim Breitner]

And merged. With the next mathlib bump we’ll see how much of https://github.com/fpvandoorn/carleson/blob/master/Carleson/ToMathlib/Height.lean and https://github.com/fpvandoorn/carleson/blob/master/Carleson/ToMathlib/MinLayer.lean can now actually be removed, or if during upstreaming things have changed a bit and there are more lemmas needed.

[Floris van Doorn]

Great! Thanks for this! That's a lot of small PRs... :amazement:

[Kevin Buzzard]

Small PRs is a great way to get stuff into mathlib these days!

[Michael Rothgang]

Yesterday, a PR bumping to recent mathlib was merged. I removed everything in Height.lean, as that had been upstreamed.
@Joachim Breitner It's not clear to me if something in MinLayer.lean can also be removed. Would you like to take a look? Thanks!

[Joachim Breitner]

I have a gut feeling that maybe we don't need the minlayer abstraction, or that it would be more natural to be defined as the preimage under height, but such gut feeling can be misleading, and it'd only be a nice-to-have gut feeling. I don't know if I'll have time to have a look soon, but it's also not really pressing for the project, is it?