rearranging indices in a summable

Stream: maths

[Chris Birkbeck]

So, I'm stuck trying to prove the following:

import data.complex.basic
open_locale big_operators

lemma sum_lemma (f: ℤ × ℤ → ℝ) (I: ℕ → finset (ℤ × ℤ)) (HI: ∀ (y : ℤ × ℤ), ∃! (i : ℕ), y ∈ I (i) )  :
summable f ↔ summable (λ ( n : ℕ), ∑ x in I (n), f x)  :=
begin
sorry,
end

Now, if I've understood summable correctly then this should hopefully be true as I am essentially reordering the index (i.e. I want to break up the sum intro a sum over some finite (disjoint) subsets) and hopefully I have enough hypotheses for this. I've been looking through the infinte_sum file and I'm struggling to find something to prove this with. I thought about using equiv.summable_iff but I can't see how to write down an equivalent indexing set that would easily break up into the sum on the rhs. So, I wanted to see if anyone has any ideas how one might try and prove this (provided I've not missunderstood something and its actually false!).

[Sebastien Gouezel]

I don't think your lemma is true. Since ℤ × ℤ does not really play a role in your statement, let me replace it by ℕ. Take f n = (-1)^n (which is not summable) and I n = {2 n, 2 n + 1} (so that the sum of f on each I n is zero). Then summable (λ ( n : ℕ), ∑ x in I (n), f x) is true and summable f is false.

[Chris Birkbeck]

Oh maybe I'm confused about what summable is then. I though it was the same as absolutely convergent (?)

[Sebastien Gouezel]

Essentially yes. My function f is not absolutely convergent, but the sums over the different I n are, as they are all zero.

[Sebastien Gouezel]

The left to right implication is true, but the right to left is not.

[Chris Birkbeck]

But what you say makes sence, so maybe I need to think a bit more about how to state this. Thanks!

[Sebastien Gouezel]

If the function is nonnegative, your equivalence is true.

[Chris Birkbeck]

ah yes, the function I have in mind is non-negative, so maybe that is the hyp I forgot

[Chris Birkbeck]

So maybe what I want is:

import data.complex.basic
open_locale big_operators

lemma sum_lemma (f: ℤ × ℤ → ℝ≥0) (I: ℕ → finset (ℤ × ℤ)) (HI: ∀ (y : ℤ × ℤ), ∃! (i : ℕ), y ∈ I (i) )  :
summable f ↔ summable (λ ( n : ℕ), ∑ x in I (n), f x)  :=
begin
sorry,
end

[Chris Birkbeck]

So, now that I think of it there is this summable_sigma_of_nonneg lemma in the ennreal file. It sort of looks like what I want but I dont know what sigmas are? can this be intepreted as a (disjoint) union? I which case I think this might almost be the result I want.

[Kevin Buzzard]

Yes, Σ x, β x is disjoint union. If beta is a map from X to Type (i.e. a collection of sets $\beta_x$ as $x$ runs through some index set $X$) then to give a term of type Σ x, β x is to give a pair consisting of x : X and y : β x, so if you think about it then this is just the same as giving an element of the disjoint union.

[Chris Birkbeck]

Ah great, I'll see if I can get it to work with this then. Thanks!