combinatorial lemma 9.8

Stream: condensed mathematics

[Johan Commelin]

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]

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]

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]

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]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Peter Scholze]

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]

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

[Johan Commelin]

ooh, maybe I now understand the idea. Thanks.

[Johan Commelin]

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

[Peter Scholze]

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

[Peter Scholze]

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]

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

[Johan Commelin]

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]

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]

But I'm done for the day

[Peter Scholze]

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

[Peter Scholze]

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]

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]

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

[Peter Scholze]

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<r<1$, 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]

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]

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]

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]

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]

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]

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]

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]

Now the naive inequality gives the rest

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Johan Commelin]

Congratulations!!

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

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]

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]

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]

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]

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

[Kevin Buzzard]

Yeah we need a new stream for that one

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@Chris Hughes Do you think you could help here?

[Chris Hughes]

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

[Johan Commelin]

/-- 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]

We need something like this

[Johan Commelin]

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

[Johan Commelin]

I saw that there is list.argmin which might help

[Chris Hughes]

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]

No they shouldn't be the same

[Johan Commelin]

Sorry, I see now that the docstring was wrong

[Johan Commelin]

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

[Johan Commelin]

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]

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]

Can you add the imports and notation?

[Johan Commelin]

sure, 1 sec

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

I did half of the step exists_partition -> lem98_int

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Ok, thanks for the pointers.

[Heather Macbeth]

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]

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

[Johan Commelin]

I killed some easy sorries (-;

[Johan Commelin]

@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]

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

[Johan Commelin]

And then gradually fill in the remaining sorrys.

[Heather Macbeth]

Great, thank you for tracking down those decidability instances!

[Heather Macbeth]

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]

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]

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]

@Heather Macbeth I hope so (-;

[Johan Commelin]

We'll find out

[Johan Commelin]

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

[Johan Commelin]

It should be fine

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@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]

@Heather Macbeth never mind, I've fixed it

[Johan Commelin]

The proof of 9.8 is now completed, modulo 9.7.