tsum_lt?

Stream: Is there code for X?

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

I am also going to remove the unnecessary assumption summable f

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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 ∑'

[Damiano Testa]

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

Thanks for your suggestions!

[Damiano Testa]

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

[Adam Topaz]

Oh, just parens missing

[Adam Topaz]

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]

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

[Adam Topaz]

I just upgraded mathlib....

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe I'm on an old mathlib then!

[Adam Topaz]

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

[Adam Topaz]

All good now :)

[Adam Topaz]

Oh, we don't even have tsum_pos :(

[Damiano Testa]

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]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

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]

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

[Eric Wieser]

Fixed in #5993

[Damiano Testa]

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

[Eric Wieser]

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]

Alright, that pr is now merged

[Damiano Testa]

Thank you very much!

[Damiano Testa]

I created a PR introducing these lemmas: #6017

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

[Eric Wieser]

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)