Zulip Chat Archive

Stream: condensed mathematics

Topic: combinatorial lemma 9.8


view this post on Zulip 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?

view this post on Zulip Peter Scholze (Feb 23 2021 at 19:33):

Regarding 9.8: The version in the lecture notes has profinite SS, but we only need finite SS 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 SS.

view this post on Zulip Johan Commelin (Feb 25 2021 at 07:26):

I have some questions about 9.8:

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

I understand the remark "decomposing any sum with terms of size at most 1 into NN 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?

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Peter Scholze (Feb 25 2021 at 12:39):

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

view this post on Zulip Johan Commelin (Feb 25 2021 at 12:39):

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

view this post on Zulip Peter Scholze (Feb 25 2021 at 12:40):

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

view this post on Zulip Peter Scholze (Feb 25 2021 at 12:41):

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

view this post on Zulip Peter Scholze (Feb 25 2021 at 12:42):

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

view this post on Zulip Johan Commelin (Feb 25 2021 at 12:43):

ooh, maybe I now understand the idea. Thanks.

view this post on Zulip Johan Commelin (Feb 25 2021 at 12:43):

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

view this post on Zulip 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 :-)

view this post on Zulip 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 R\mathbb R to Z\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!

view this post on Zulip Peter Scholze (Feb 25 2021 at 12:48):

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

view this post on Zulip Johan Commelin (Feb 25 2021 at 21:37):

There is 1 sorry left, namely the lemma about arranging a sum whose terms are all 1\le 1 into NN 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=aAsupi<Na(li)li(S(1r)N+1)d = \sum_{a \in A} \sup_{i < N} \frac{\|a(l_i)\|}{\|l_i\|} \cdot \left( \frac{|S|}{(1-r') \cdot N} + 1\right)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 25 2021 at 21:38):

But I'm done for the day

view this post on Zulip Peter Scholze (Feb 25 2021 at 22:02):

Wait, dd is not allowed to depend on SS!

view this post on Zulip Peter Scholze (Feb 25 2021 at 22:04):

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

view this post on Zulip Peter Scholze (Feb 25 2021 at 22:06):

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

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Feb 25 2021 at 22:14):

In any case, here's what I have in mind. You have all those term Tn[s]T^{-n} [s], each has weight rnr^n where 0<r<10<r<1, and in total they have weight c\leq c. You want to distribute this into NN parts such that each part has weight c/N+1\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 11.

view this post on Zulip Johan Commelin (Feb 26 2021 at 05:47):

Aha, what I did was the following. We have x=x0+aAaxax = x_0 + \sum_{a \in A} ax_a. Now apply the special case of Λ=Z\Lambda = \Z to the xax_a to find xa=ya,1++ya,Nx_a = y'_{a,1} + \dots + y'_{a,N} with ya,jxa/N+1\|y'_{a,j}\| \le \|x_a\|/N + 1. Then define yj=x0+aAaya,jy_j = x_0 + \sum_{a \in A} ay'_{a,j}.

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

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

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

view this post on Zulip Johan Commelin (Feb 26 2021 at 05:56):

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

Lemma. Let a ⁣:ΛZa \colon \Lambda \to \Z be some homomorphism, and yMr(S)cy \in \mathcal{M}_{r'}(S)_{\le c}. Let {l1,,lm}\{l_1, \dots, l_m\} generate the norm of Λ\Lambda. Then ayHom(Λ,Mr(S))δay \in \mathrm{Hom}(\Lambda, \mathcal{M}_{r'}(S))_\delta, where δ=supi=1,,ma(li)lic\delta = \sup_{i=1,\dots,m} \frac{\|a(l_i)\|}{\|l_i\|} \cdot c.

view this post on Zulip Johan Commelin (Feb 26 2021 at 06:01):

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

view this post on Zulip Johan Commelin (Feb 26 2021 at 06:03):

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

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

view this post on Zulip 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(λi)=Nx0(λi)+aAa(λi)xa||x(\lambda_i)||=N||x_0(\lambda_i)|| + \sum_{a\in A} ||a(\lambda_i)|| ||x_a||.

view this post on Zulip Peter Scholze (Feb 26 2021 at 08:27):

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

view this post on Zulip Peter Scholze (Feb 26 2021 at 08:30):

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

view this post on Zulip Peter Scholze (Feb 26 2021 at 08:31):

Now the naive inequality gives the rest

view this post on Zulip Johan Commelin (Feb 26 2021 at 08:35):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 26 2021 at 15:59):

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

view this post on Zulip 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 (-;

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Feb 27 2021 at 05:49):

Congratulations!!

view this post on Zulip Johan Commelin (Feb 27 2021 at 06:04):

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

view this post on Zulip Johan Commelin (Feb 27 2021 at 07:42):

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

view this post on Zulip Peter Scholze (Feb 27 2021 at 08:17):

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

view this post on Zulip Peter Scholze (Feb 27 2021 at 08:20):

Consider some positive integer nn and finitely many positive real numbers xix_i, iIi\in I, all xi1x_i\leq 1. Let s=iIxis=\sum_{i\in I} x_i. Show that you can find a partition of II into nn sets I1,,InI_1,\ldots,I_n such that all sj=iIjxis_j=\sum_{i\in I_j} x_i (j=1,,nj=1,\ldots,n) satisfy sjs/N+1s_j\leq s/N+1. (Or slightly better, that all sjs_j differ by at most 11.)

view this post on Zulip 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 SS, and then lexicographically ordering S×NS \times \N.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 09:43):

Yeah we need a new stream for that one

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 27 2021 at 09:56):

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

view this post on Zulip Johan Commelin (Feb 27 2021 at 09:56):

@Chris Hughes Do you think you could help here?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:00):

We need something like this

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:00):

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

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:01):

I saw that there is list.argmin which might help

view this post on Zulip 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))

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:22):

No they shouldn't be the same

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:22):

Sorry, I see now that the docstring was wrong

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:23):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Feb 27 2021 at 10:30):

Can you add the imports and notation?

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:30):

sure, 1 sec

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 27 2021 at 10:35):

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

view this post on Zulip 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.

view this post on Zulip 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],
        exact add_le_add (le_refl _) (le_trans (nsmul_le_nsmul_of_le_right h _) hs) },
      { use [b, finset.mem_insert_of_mem hbs],
        exact add_le_add (le_of_not_le h) hs } },
    { use a,
      simp [(finset.eq_empty_or_nonempty s).resolve_right hs] } },
end

view this post on Zulip Johan Commelin (Feb 27 2021 at 14:06):

I did half of the step exists_partition -> lem98_int

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Feb 27 2021 at 18:00):

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

view this post on Zulip Johan Commelin (Feb 27 2021 at 18:03):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 27 2021 at 18:04):

Ok, thanks for the pointers.

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Mar 03 2021 at 05:51):

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

view this post on Zulip Johan Commelin (Mar 03 2021 at 06:59):

I killed some easy sorries (-;

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 03 2021 at 07:18):

And then gradually fill in the remaining sorrys.

view this post on Zulip Heather Macbeth (Mar 03 2021 at 07:20):

Great, thank you for tracking down those decidability instances!

view this post on Zulip 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)!

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 03 2021 at 16:17):

@Heather Macbeth I hope so (-;

view this post on Zulip Johan Commelin (Mar 03 2021 at 16:17):

We'll find out

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 03 2021 at 16:18):

It should be fine

view this post on Zulip Johan Commelin (Mar 03 2021 at 17:29):

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

view this post on Zulip Johan Commelin (Mar 03 2021 at 17:32):

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

view this post on Zulip Johan Commelin (Mar 10 2021 at 07:11):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 10 2021 at 09:26):

@Heather Macbeth never mind, I've fixed it

view this post on Zulip 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