Stream: Is there code for X?

Topic: tsum_lt?

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


Adam Topaz (Jan 31 2021 at 20:25):

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

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...

Damiano Testa (Jan 31 2021 at 20:31):

I am also going to remove the unnecessary assumption summable f

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.

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...

Kevin Buzzard (Jan 31 2021 at 20:34):

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

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...

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.

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


red squiggle under the first ∑'

Damiano Testa (Jan 31 2021 at 20:36):

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

Damiano Testa (Jan 31 2021 at 20:36):

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

Adam Topaz (Jan 31 2021 at 20:36):

Oh, just parens missing

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


Kevin Buzzard (Jan 31 2021 at 20:37):

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

Kevin Buzzard (Jan 31 2021 at 20:37):

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

Kevin Buzzard (Jan 31 2021 at 20:37):

Maybe I'm on an old mathlib then!

Adam Topaz (Jan 31 2021 at 20:38):

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

All good now :)

Adam Topaz (Jan 31 2021 at 20:42):

Oh, we don't even have tsum_pos :(

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!

Damiano Testa (Jan 31 2021 at 21:13):

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

Eric Wieser (Jan 31 2021 at 22:37):

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

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


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.

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)


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!

Eric Wieser (Feb 01 2021 at 11:23):

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

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

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...

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

Fixed in #5993

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?

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


Eric Wieser (Feb 01 2021 at 23:02):

Alright, that pr is now merged

Damiano Testa (Feb 02 2021 at 06:40):

Thank you very much!

Damiano Testa (Feb 03 2021 at 08:22):

I created a PR introducing these lemmas: #6017

lemma tsum_lt_congr {i : ℕ} {f g : ℕ → ℝ} (h : f < g) (hf : summable f) (hg : summable g) :