Zulip Chat Archive

Stream: Is there code for X?

Topic: tsum_lt?


view this post on Zulip Damiano Testa (Jan 31 2021 at 20:22):

Dear All,

I am interested in proving the lemma below, but I am having a hard time. Can someone help me find a proof?

Thank you very much!

import topology.algebra.infinite_sum

lemma tsum_lt (f g :   ) (h0 :  (b : ), 0  f b) (h :  (b : ), f b  g b)
  (hg: summable g) {i : } (hi : f i < g i) :
  ∑' n, f n < ∑' n, g n :=
begin
  sorry
end

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:25):

There's docs#tsum_le_tsum which gets you almost all the way there :)

view this post on Zulip Damiano Testa (Jan 31 2021 at 20:30):

I had seen it, but I got stuck when I wanted to extract an element from the sum...

view this post on Zulip Damiano Testa (Jan 31 2021 at 20:31):

I am also going to remove the unnecessary assumption summable f

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 20:33):

Yeah this is still a bit messy even after tsum_le_tsum :-/ I would be tempted to define a new sequence h which is 0 away from i, and g(i)-f(i) at i, and then apply tsum_le_tsum to (f+h) and g.

view this post on Zulip Damiano Testa (Jan 31 2021 at 20:34):

Ok, it seems a bit more laborious than I would have liked, but maybe it is simply a reflection of the fact that the API is not there yet...

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 20:34):

Presumably there's some lemma which gives you summable f straight back after you removed it.

view this post on Zulip Damiano Testa (Jan 31 2021 at 20:35):

Well, the summable f follows from summable_of_nonneg_of_le which is already there... so that is only a minor issue...

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 20:35):

API: Right -- there don't seem to be any results which give you that a sum is less than another sum. My proposal was the simplest way around this which I could think of.

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:36):

I'm getting an error with this code @Damiano Testa :

5:3: failed to synthesize type class instance for
f g :   ,
h0 :  (b : ), 0  f b,
h :  (b : ), f b  g b,
hg : summable g,
i : ,
hi : f i < g i
 add_comm_monoid Prop

red squiggle under the first ∑'

view this post on Zulip Damiano Testa (Jan 31 2021 at 20:36):

Anyway, I'll give up for tonight and try again tomorroq!

Thanks for your suggestions!

view this post on Zulip Damiano Testa (Jan 31 2021 at 20:36):

Adam, that is weird: it works for me with only that import...

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:36):

Oh, just parens missing

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:37):

import topology.algebra.infinite_sum

lemma tsum_lt (f g :   ) (h0 :  (b : ), 0  f b) (h :  (b : ), f b  g b)
  (hg: summable g) {i : } (hi : f i < g i) :
  (∑' n, f n) < ∑' n, g n :=
begin
  sorry
end

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 20:37):

The code works fine for me too. Are you on an old mathlib?

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:37):

I just upgraded mathlib....

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 20:37):

I think Eric or someone changed priorities of sums a week or two ago.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 20:37):

Maybe I'm on an old mathlib then!

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:38):

Oh, I upgraded mathlib, but didn't restart the server.

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:38):

All good now :)

view this post on Zulip Adam Topaz (Jan 31 2021 at 20:42):

Oh, we don't even have tsum_pos :(

view this post on Zulip Damiano Testa (Jan 31 2021 at 21:12):

Ok, I am glad that it was not just me, then!

If no one else does it earlier, I may try to prove some of these results tomorrow!

view this post on Zulip Damiano Testa (Jan 31 2021 at 21:13):

(If someone else wants to do it, though, I would be very grateful!)

view this post on Zulip Eric Wieser (Jan 31 2021 at 22:37):

It was Johan, but I was the one who jogged his memory into fixing it

view this post on Zulip Damiano Testa (Feb 01 2021 at 10:45):

Below is a proof of tsum_lt.

In case anyone feels like they want to simplify these proofs, please go ahead! Otherwise, I might open a PR to include them somewhere.

import topology.instances.ennreal

lemma tsum_ite_eq_add {f :   } (hf : summable f) (i : ) (a : ) :
  ∑' n, ((ite (n = i) a 0) + f n) = a + ∑' n, f n :=
begin
  rw [tsum_add a, _ hf, @tsum_eq_single  _ _ _ _ _ i],
  { split_ifs; refl },
  { exact λ (j : ) (ji : ¬ j = i), @if_neg _ _ ji _ _ _ },
  { convert has_sum_ite_eq i a,
    refine funext (λ x, _),
    congr }
end

lemma tsum_eq {f g :   } (hfg :  n, f n = g n) :
  ∑' n, f n = ∑' n, g n :=
by simp_rw [hfg]

lemma tsum_ite_eq_extract {f :   } (hf : summable f) (i : ) :
  ∑' n, f n = f i + ∑' n, ite (n  i) (f n) 0 :=
by rw [ tsum_ite_eq_add (hf.summable_of_eq_zero_or_self (λ j, _)) i, tsum_eq (λ j, _)];
  by_cases ji : j = i; simp [ji]

lemma tsum_lt {f g :   } (h :  (b : ), f b  g b)
  (hf: summable f) (hg: summable g) {i : } (hi : f i < g i) :
  ∑' n, f n < ∑' n, g n :=
begin
  rw [tsum_ite_eq_extract hf i, tsum_ite_eq_extract hg i],
  refine add_lt_add_of_lt_of_le hi (tsum_le_tsum (λ j, _) _ _),
  by_cases ji : j = i; simp [ji]; exact h j,
  { refine hf.summable_of_eq_zero_or_self (λ j, _),
    by_cases ji : j = i; simp [ji] },
  { refine hg.summable_of_eq_zero_or_self (λ j, _),
    by_cases ji : j = i; simp [ji] }
end

lemma tsum_lt_of_nonneg {f g :   } (h0 :  (b : ), 0  f b) (h :  (b : ), f b  g b)
  (hg: summable g) {i : } (hi : f i < g i) :
  ∑' n, f n < ∑' n, g n :=
tsum_lt h (summable_of_nonneg_of_le h0 h hg) hg hi

view this post on Zulip Damiano Testa (Feb 01 2021 at 11:08):

I slightly golfed the proofs and changed the statement of tsum_lt: what was tsum_lt at the beginning of the thread is now tsum_lt_of_nonneg.

view this post on Zulip Eric Wieser (Feb 01 2021 at 11:15):

tsum_congr might be a good name for tsum_eq, especially since it can be proved as:

lemma tsum_congr {f g :   } (hfg :  n, f n = g n) :
  ∑' n, f n = ∑' n, g n :=
congr_arg tsum (funext hfg)

view this post on Zulip Damiano Testa (Feb 01 2021 at 11:18):

Eric, thank you very much for always checking my stuff! I like your suggestion and I updated the code above!

view this post on Zulip Eric Wieser (Feb 01 2021 at 11:23):

Similarly, you seem to be suffering because docs#tsum_ite_eq is missing a decidable assumption

view this post on Zulip Eric Wieser (Feb 01 2021 at 11:24):

Which means it only applies to classical.dec, and not to the nat.decidable_eq that your proof uses

view this post on Zulip Damiano Testa (Feb 01 2021 at 11:28):

I have open_locale classical in my actual file, although, since I could erase it and the proofs still went through, I did not include it in this snippet. What could I simplify, using classical? I know that some things become easier, but I do not really have a feel for what...

view this post on Zulip Eric Wieser (Feb 01 2021 at 11:35):

Almost all of your tsum_ite_eq_add proof should be solved by docs#tsum_ite_eq, but it's not because the instances don't unify

view this post on Zulip Eric Wieser (Feb 01 2021 at 11:36):

Fixed in #5993

view this post on Zulip Damiano Testa (Feb 01 2021 at 11:37):

Ah, thank you so much! This means that, once your PR gets accepted, the proofs here can be simplified, right?

view this post on Zulip Eric Wieser (Feb 01 2021 at 11:38):

Yes. In the meantime, you can add

-- fixed version of tsum_ite_eq until 5993 is merged
@[simp] lemma tsum_ite_eq' (i : ) (a : ) :
  ∑' n, (ite (n = i) a 0) = a :=
begin
  convert tsum_ite_eq i a,
  funext, congr,
end

view this post on Zulip Eric Wieser (Feb 01 2021 at 23:02):

Alright, that pr is now merged

view this post on Zulip Damiano Testa (Feb 02 2021 at 06:40):

Thank you very much!

view this post on Zulip Damiano Testa (Feb 03 2021 at 08:22):

I created a PR introducing these lemmas: #6017

Eric, I took advantage of your simplifications, but there are certainly more simplifications to be made!

view this post on Zulip Eric Wieser (Feb 03 2021 at 14:24):

I think the best statement of this lemma might actually be:

lemma tsum_lt_congr {i : } {f g :   } (h : f < g) (hf : summable f) (hg : summable g) :
  ∑' n, f n < ∑' n, g n :=

although the lemmas to make this easy to work with are missing (xref this thread)


Last updated: May 07 2021 at 22:14 UTC