## Stream: condensed mathematics

### Topic: combinatorial lemma 9.8

#### Johan Commelin (Feb 23 2021 at 09:23):

We do not yet have all the ingredients to prove 9.7. But if we accept it as a black box, I think we can at least start working on 9.8. Is there anyone who wants to take a shot at it?

#### Peter Scholze (Feb 23 2021 at 19:33):

Regarding 9.8: The version in the lecture notes has profinite $S$, but we only need finite $S$ in the version of the proof following the blueprint. So you should ignore the first few lines of the proof regarding the reduction to finite $S$.

#### Johan Commelin (Feb 25 2021 at 07:26):

I have some questions about 9.8:

• The second display on p62 contains a factor $\|x_a(\lambda_i)\|$. This doesn't typecheck for me, and I guess it should just be $\|x_a\|$, right?
• The norm of $x_a$ is bounded above by $|S| \cdot r'/(1-r')$. I don't understand how distributing the sum over $N$ partial sums gets rid of this dependence.

I understand the remark "decomposing any sum with terms of size at most 1 into $N$ such partial sums whose sums differ by at most 1". But I don't see how to apply it in this situation. Why do those partial sums have the required bound on their norms?

#### Johan Commelin (Feb 25 2021 at 12:23):

Apart from the confusion above, 9.8 is now almost done. (Of course it takes 9.7 as black box input, so there is another sorry there.)

#### Johan Commelin (Feb 25 2021 at 12:24):

@Peter Scholze Is the constant d that appears in the statement of 9.8 important? Should we track its size?

#### Peter Scholze (Feb 25 2021 at 12:39):

The occurence of $||x_a(\lambda_i)||$ is indeed a typo, it should be $||x_a||$.

#### Johan Commelin (Feb 25 2021 at 12:39):

Ok, I'll fix those in the various TeX sources

#### Peter Scholze (Feb 25 2021 at 12:40):

For the last step: are you fine with the reduction to $\Lambda=\mathbb Z$?

#### Peter Scholze (Feb 25 2021 at 12:41):

The task is to write any individual $x_a$ as a sum of $N$ terms, all of which are size $\leq ||x_a||/N+1$

#### Peter Scholze (Feb 25 2021 at 12:42):

About the constant $d$: The size is not really important, it only influences some "secondary" constants

#### Johan Commelin (Feb 25 2021 at 12:43):

ooh, maybe I now understand the idea. Thanks.

#### Johan Commelin (Feb 25 2021 at 12:43):

I'll think through it carefully, and then try to convince lean

#### Peter Scholze (Feb 25 2021 at 12:45):

OK, great! This is called the key lemma in the manuscript, so I hope it will work :-)

#### Peter Scholze (Feb 25 2021 at 12:48):

By the way, the fact that you have to include some nontrivial chunks of "convex geometry" for the proof of 9.7 made me realize that another reason this funny reduction from $\mathbb R$ to $\mathbb Z$ is necessary is that after this reduction, one can use convex geometry (combined with lattice theory). In essence, one discretizes a problem in order to reduce a non-convex problem to a convex problem!

#### Peter Scholze (Feb 25 2021 at 12:48):

I wonder whether this is some well-known method in some areas?

#### Johan Commelin (Feb 25 2021 at 21:37):

There is 1 sorry left, namely the lemma about arranging a sum whose terms are all $\le 1$ into $N$ such sums.

For d, I get the following constant:

  let d : ℝ≥0 :=
∑ a in A, finset.univ.sup (λ i, ↑(a (l i)).nat_abs / nnnorm (l i)) *
(fintype.card S * (1 - r')⁻¹ / N + 1),


In TeX: $d = \sum_{a \in A} \sup_{i < N} \frac{\|a(l_i)\|}{\|l_i\|} \cdot \left( \frac{|S|}{(1-r') \cdot N} + 1\right)$

#### Johan Commelin (Feb 25 2021 at 21:38):

I can't seem to manage to get it down to the constant in the text. But maybe I'm missing some trick.

#### Johan Commelin (Feb 25 2021 at 21:38):

But I'm done for the day

#### Peter Scholze (Feb 25 2021 at 22:02):

Wait, $d$ is not allowed to depend on $S$!

#### Peter Scholze (Feb 25 2021 at 22:04):

You are right that in the text I forgot to divide by $||\lambda_i||$, but I'm confused where you get that factor $\frac{|S|}{(1-r')N}$ which would be very bad

#### Peter Scholze (Feb 25 2021 at 22:06):

Ah, I have the feeling that you are doing some optimization in any power of $T^{-1}$ individually when you try to do that splitting. But that's no good, you need to consider all powers of $T^{-1}$ at the same time in that "pigeonholing" process.

#### Peter Scholze (Feb 25 2021 at 22:12):

uhhh... hmm no maybe that is not the issue. well, I'm a little confused about what exactly you're doing.

#### Peter Scholze (Feb 25 2021 at 22:14):

In any case, here's what I have in mind. You have all those term $T^{-n} [s]$, each has weight $r^n$ where $0, and in total they have weight $\leq c$. You want to distribute this into $N$ parts such that each part has weight $\leq c/N+1$. You do that by always putting each new piece into the part of smallest weight; this way, the minimum and the maximum always differ by at most $1$.

#### Johan Commelin (Feb 26 2021 at 05:47):

Aha, what I did was the following. We have $x = x_0 + \sum_{a \in A} ax_a$. Now apply the special case of $\Lambda = \Z$ to the $x_a$ to find $x_a = y'_{a,1} + \dots + y'_{a,N}$ with $\|y'_{a,j}\| \le \|x_a\|/N + 1$. Then define $y_j = x_0 + \sum_{a \in A} ay'_{a,j}$.

We want to show $\|y_i\| \le \|x\|/N + d$ for some $d$. Maybe here I'm taking a wrong step, but my reasoning was:

• $\|x_0\| \le \|x\|/N$
• so we want to show $\|\sum_{a \in A}ay'_{a,j}\| \le d$, for each $j = 1,\dots,N$

Does that make sense? Or do I somehow need to do something smarter than just triangle inequality?

#### Johan Commelin (Feb 26 2021 at 05:56):

So, let's fix a $j \in \{1,\dots,N\}$. I continued by $\|\sum_{a \in A} ay'_{a,j}\| \le \sum_{a \in A} \|ay'_{a,j}\|$. So now we want to understand $\|ay'_{a,j}\|$.
Here I used the following lemma.

Lemma. Let $a \colon \Lambda \to \Z$ be some homomorphism, and $y \in \mathcal{M}_{r'}(S)_{\le c}$. Let $\{l_1, \dots, l_m\}$ generate the norm of $\Lambda$. Then $ay \in \mathrm{Hom}(\Lambda, \mathcal{M}_{r'}(S))_\delta$, where $\delta = \sup_{i=1,\dots,m} \frac{\|a(l_i)\|}{\|l_i\|} \cdot c$.

#### Johan Commelin (Feb 26 2021 at 06:01):

Now we apply this lemma to $ay'_{a,j}$, with $c = \|x_a\|/N+1$. This gives me the bound
$\|ay'_{a,j}\| \le \sup_i \frac{\|a(l_i)\|}{\|l_i\|} \cdot (\|x_a\|/N + 1)$.

#### Johan Commelin (Feb 26 2021 at 06:03):

Finally, $\|x_a\|$ can be bound by $|S| \cdot \frac{r'}{1 - r'}$, since termwise we have $x_a \le \sum_{s,n} (r')^n$.

(But in lean I was lazy, and ignored the fact that we sum from $n \ge 1$ instead of $n \ge 0$, so I get the bound $|S| \cdot \frac{1}{1 - r'}$.)

#### Peter Scholze (Feb 26 2021 at 08:25):

Ah! Well, I think you did not make good use of this "same-sign" property, more specifically the equality $||x(\lambda_i)||=N||x_0(\lambda_i)|| + \sum_{a\in A} ||a(\lambda_i)|| ||x_a||$.

#### Peter Scholze (Feb 26 2021 at 08:27):

To show $||y_j||\leq ||x||/N + d$, we can evaluate at any $\lambda_i$, so we have to show $||y_j(\lambda_i)||\leq ||x(\lambda_i)||/N + d ||\lambda_i||$ for all $i$.

#### Peter Scholze (Feb 26 2021 at 08:30):

Now use that equality. Then both sides get one term $||x_0(\lambda_i)||$. On the left, the rest is bounded by $\sum_{a\in A} ||a(\lambda_i)|| ||y_{a,j}||$. On the right, we still have $\sum_{a\in A} ||a(\lambda_i)|| ||x_a||/N + d ||\lambda_i||$.

#### Peter Scholze (Feb 26 2021 at 08:31):

Now the naive inequality gives the rest

#### Johan Commelin (Feb 26 2021 at 08:35):

Ooh, I see. That great! Let me try to implement this.

#### Johan Commelin (Feb 26 2021 at 15:58):

This is working well. Thanks for correcting my understanding. There are a couple of sorrys left in the proof, but the are all math-trivial, and should be pretty lean-trivial.

#### Johan Commelin (Feb 26 2021 at 15:59):

And there is still the outstanding sorry for the case $\Lambda = \Z$. That one isn't lean-trivial (-;

#### Johan Commelin (Feb 26 2021 at 16:00):

If someone else wants to take a look, please go ahead. I'm a bit exhausted by this proof now (-;

#### Peter Scholze (Feb 26 2021 at 21:26):

Glad it works! A propos exhaustion: www.math.uni-bonn.de/people/scholze/Geometrization.pdf is now live :dizzy:

#### Johan Commelin (Feb 27 2021 at 05:49):

Congratulations!!

#### Johan Commelin (Feb 27 2021 at 06:04):

Today I learned: etc.pp. is an abbreviation for a sequence of abbreviations :grinning:

#### Johan Commelin (Feb 27 2021 at 07:42):

The easy sorrys are done. Now only the $\Lambda = \Z$ case is left.

#### Peter Scholze (Feb 27 2021 at 08:17):

Thanks! And great about the progress on 9.8. I think the $\Lambda=\mathbb Z$ case itself might be fun. Let me formulate a (slightly abstracted) version here, in case someone reading along wants to join:

#### Peter Scholze (Feb 27 2021 at 08:20):

Consider some positive integer $n$ and finitely many positive real numbers $x_i$, $i\in I$, all $x_i\leq 1$. Let $s=\sum_{i\in I} x_i$. Show that you can find a partition of $I$ into $n$ sets $I_1,\ldots,I_n$ such that all $s_j=\sum_{i\in I_j} x_i$ ($j=1,\ldots,n$) satisfy $s_j\leq s/N+1$. (Or slightly better, that all $s_j$ differ by at most $1$.)

#### Johan Commelin (Feb 27 2021 at 08:29):

I guess we'll need a bit of a tricky recursion to make this work. So first we need to massage the problem into the right form. (E.g. fixing a linear order on $S$, and then lexicographically ordering $S \times \N$.

#### Johan Commelin (Feb 27 2021 at 08:31):

And we don't want lean to ask us that certain sums converge at every step we take. So we should not work with terms of type Mbar r' S for most of the proof.

#### Patrick Massot (Feb 27 2021 at 08:33):

Congratulations Peter! And thanks for making sure we still have hundreds of years of formalization work ahead...

#### Kevin Buzzard (Feb 27 2021 at 09:43):

Yeah we need a new stream for that one

#### Kevin Buzzard (Feb 27 2021 at 09:47):

Maybe n=N in Peter's post? It seems to me that "greedy" does it. One can prove it by induction on n relatively simply I think. Johan can you formalise the statement in a way which will suffice to slot in to the rest of the work? What exactly do you want a partition to be? Or is this also something to be decided?

#### Kevin Buzzard (Feb 27 2021 at 09:48):

My approach won't prove the stronger result that they all differ by at most one I don't think, I don't immediately see why that's true

#### Kevin Buzzard (Feb 27 2021 at 09:50):

You just remove a subset whose sum is in [s/n,s/n+1]. Again I'm assuming n=N

#### Johan Commelin (Feb 27 2021 at 09:56):

@Kevin Buzzard right, mathematically it's not so hard. just use the greedy approach. But formalising it is non-trivial

#### Johan Commelin (Feb 27 2021 at 09:56):

Probably because I don't know how to handle well founded induction and things like that.

#### Johan Commelin (Feb 27 2021 at 09:56):

@Chris Hughes Do you think you could help here?

#### Chris Hughes (Feb 27 2021 at 09:59):

Haven't been following this thread. What is the lemma that needs to be proved? Where is the 9.8 from?

#### Johan Commelin (Feb 27 2021 at 10:00):

/-- Sends n : ℕ to the i : fin N
for which ∑ k in (finset.range n).filter (λ k, partition_tsum k = i) is minimal. -/
def partition_tsum (N : ℕ) (hN : 0 < N) (f : ℕ → ℝ≥0) : ℕ → fin N := sorry


#### Johan Commelin (Feb 27 2021 at 10:00):

We need something like this

#### Johan Commelin (Feb 27 2021 at 10:00):

Feel free to mangle it into something that is easier to formalise

#### Johan Commelin (Feb 27 2021 at 10:01):

I saw that there is list.argmin which might help

#### Chris Hughes (Feb 27 2021 at 10:13):

Something like this? Are n and N supposed to be the same?

def partition_tsum (N : ℕ) (hN : 0 < N) (f : ℕ → ℝ≥0) : fin N :=
@option.get _ ((list.fin_range N).argmin
(λ i : fin N, ∑ k in (finset.range N).filter (λ k, k = i), k))
(option.ne_none_iff_is_some.1 (mt list.argmin_eq_none.1 \$
by simp; omega))


#### Johan Commelin (Feb 27 2021 at 10:22):

No they shouldn't be the same

#### Johan Commelin (Feb 27 2021 at 10:22):

Sorry, I see now that the docstring was wrong

#### Johan Commelin (Feb 27 2021 at 10:23):

It's supposed to be the sum of the f k's that is minimal

#### Johan Commelin (Feb 27 2021 at 10:29):

def mask_fun (f : ℕ → ℝ≥0) (mask : ℕ → Prop) [∀ n, decidable (mask n)] : ℕ → ℝ≥0 :=
λ n, if mask n then f n else 0

lemma exists_partition (N : ℕ) (hN : 0 < N) (f : ℕ → ℝ≥0) (hf : ∀ n, f n ≤ 1) :
∃ (mask : fin N → ℕ → Prop) [∀ i n, decidable (mask i n)], by exactI
(∀ n, ∃! i, mask i n) ∧ (∀ i, ∑' n, mask_fun f (mask i) n ≤ (∑' n, f n) / N + 1) :=
sorry


I think this is a formal version of Peter's claim.

#### Johan Commelin (Feb 27 2021 at 10:30):

But of course this is using tsum, which is painful to work with directly. So we should take the limit over an analogous claim with finite sums.

#### Chris Hughes (Feb 27 2021 at 10:30):

Can you add the imports and notation?

sure, 1 sec

#### Johan Commelin (Feb 27 2021 at 10:32):

import data.real.nnreal
import topology.algebra.infinite_sum

open_locale nnreal

def mask_fun (f : ℕ → ℝ≥0) (mask : ℕ → Prop) [∀ n, decidable (mask n)] : ℕ → ℝ≥0 :=
λ n, if mask n then f n else 0

lemma exists_partition (N : ℕ) (hN : 0 < N) (f : ℕ → ℝ≥0) (hf : ∀ n, f n ≤ 1) :
∃ (mask : fin N → ℕ → Prop) [∀ i n, decidable (mask i n)], by exactI
(∀ n, ∃! i, mask i n) ∧ (∀ i, ∑' n, mask_fun f (mask i) n ≤ (∑' n, f n) / N + 1) :=
sorry


#### Johan Commelin (Feb 27 2021 at 10:35):

This is now the contents of src/partition.lean on the liquid repo

#### Johan Commelin (Feb 27 2021 at 10:37):

I need to go do something else now, but there are now two steps.

1. Removing the sorry in exists_partition.
2. And using that to prove lem98_int. For this, it may be useful to use Mbar.of_mask after turning x : Mbar r' S into a function nat -> nnreal.

#### Chris Hughes (Feb 27 2021 at 11:30):

This lemma might be handy.

lemma exists_smul_le_sum {α M : Type*} [linear_ordered_cancel_add_comm_monoid M] (s : finset α)
(hs : s.nonempty) (f : α → M) : ∃ a ∈ s, finset.card s •ℕ f a ≤ ∑ x in s, f x :=
begin
classical,
induction s using finset.induction_on with a s has ih,
{ cases hs with a ha,
exact ⟨a, by simp *⟩ },
{ simp only [finset.card_insert_of_not_mem has, finset.sum_insert has, succ_nsmul],
by_cases hs : s.nonempty,
{ rcases ih hs with ⟨b, hbs, hs⟩,
by_cases f a ≤ f b,
{ use [a, by simp],
{ use [b, finset.mem_insert_of_mem hbs],
{ use a,
simp [(finset.eq_empty_or_nonempty s).resolve_right hs] } },
end


#### Johan Commelin (Feb 27 2021 at 14:06):

I did half of the step exists_partition -> lem98_int

#### Johan Commelin (Feb 27 2021 at 17:42):

We probably also need a lemma of the following shape:

lemma tsum_prod_eq_sum_tsum (S : Type*) [fintype S] (f : S × ℕ → ℝ≥0) :
∑' x, f x = ∑ s, ∑' n, f (s, n) := sorry


#### Sebastien Gouezel (Feb 27 2021 at 18:00):

This will not be true unless you add suitable summability assumptions...

#### Johan Commelin (Feb 27 2021 at 18:03):

Aah, sure. All the tsums on the right are summable

#### Johan Commelin (Feb 27 2021 at 18:04):

Is this better?

lemma tsum_prod_eq_sum_tsum (S : Type*) [fintype S] (f : S × ℕ → ℝ≥0) (hf : ∀ s, summable (λ n, f (s, n))) :
∑' x, f x = ∑ s, ∑' n, f (s, n) := sorry


#### Sebastien Gouezel (Feb 27 2021 at 18:04):

Once you have these assumptions, this will follow from tsum_sigma (or tsum_sigma') and tsum_fintype.

#### Johan Commelin (Feb 27 2021 at 18:04):

Ok, thanks for the pointers.

#### Heather Macbeth (Mar 03 2021 at 05:02):

I made a stab at setting up the recursion for exists_partition -- see
https://github.com/leanprover-community/lean-liquid/compare/exists-partition
There are various sorries, basically of three kinds: (a) hopefully-trivial algebra, (b) the extension from partial sums to series, (c) instance inference for decidability/nonemptiness.

I will try again tomorrow night or the next day, but in the meantime, anyone else should feel free to work on it!

#### Johan Commelin (Mar 03 2021 at 05:51):

@Heather Macbeth great! thanks a lot! I'll look at it after breaking my fast :breakfast:

#### Johan Commelin (Mar 03 2021 at 06:59):

I killed some easy sorries (-;

#### Johan Commelin (Mar 03 2021 at 07:17):

@Heather Macbeth btw, I think I messed up a bit, I thought I had moved exists_partition to its own file, but I only copied it.
src/partition.lean

#### Johan Commelin (Mar 03 2021 at 07:17):

I think we can just move all your code to that file, and merge it into master.

#### Johan Commelin (Mar 03 2021 at 07:18):

And then gradually fill in the remaining sorrys.

#### Heather Macbeth (Mar 03 2021 at 07:20):

Great, thank you for tracking down those decidability instances!

#### Heather Macbeth (Mar 03 2021 at 07:29):

Johan Commelin said:

I think we can just move all your code to that file, and merge it into master.

Moved (and merged)!

#### Johan Commelin (Mar 03 2021 at 10:17):

Heather Macbeth said:

There are various sorries, basically of three kinds: (a) hopefully-trivial algebra, (b) the extension from partial sums to series, (c) instance inference for decidability/nonemptiness.

Only one sorry remains in src/partition.lean, namely (b).

#### Heather Macbeth (Mar 03 2021 at 16:05):

I looked up all the summability lemmas and pushed an outline for this -- just a couple of algebra sorries left!

I added a summability hypothesis to f in exists_partition, is that ok?

#### Johan Commelin (Mar 03 2021 at 16:17):

@Heather Macbeth I hope so (-;

We'll find out

#### Johan Commelin (Mar 03 2021 at 16:18):

For our application we multiply with r^n, so termwise we are less than the geometric series.

#### Johan Commelin (Mar 03 2021 at 16:18):

It should be fine

#### Johan Commelin (Mar 03 2021 at 17:29):

@Heather Macbeth I fixed those sorries. Thanks a lot for doing the hard part!

#### Johan Commelin (Mar 03 2021 at 17:32):

This is cool, because it means that 9.8 is now almost done (modulo 9.7).

#### Johan Commelin (Mar 10 2021 at 07:11):

I've moved the sorry's about lemma 9.7 to a new file lem97.lean.

#### Johan Commelin (Mar 10 2021 at 08:04):

@Heather Macbeth In the proof of exists_partition it seems that you didn't need to prove that the mask_fun fs were summable, right? But do you think it is easy to export a summability witness anyway? That might be useful in the proof of lem98_int

#### Johan Commelin (Mar 10 2021 at 09:26):

@Heather Macbeth never mind, I've fixed it

#### Johan Commelin (Mar 10 2021 at 09:26):

The proof of 9.8 is now completed, modulo 9.7.

Last updated: May 09 2021 at 23:10 UTC