sum of row sums equals sum of column sums

Stream: Is there code for X?

[Kevin Buzzard]

import topology.algebra.infinite_sum

/-- sum of row sums equals sum of column sums -/
lemma summable_snd_of_summable_fst {α β: Type*} (F : α → β → ℝ) (h_nonneg : ∀ n k, 0 ≤ F n k)
  (h_rows : ∀ n, summable (λ k, F n k)) (h_cols : ∀ k, summable (λ n, F n k))
  (h_col_row : summable (λ k, ∑' n, F n k)) : summable (λ n, ∑' k, F n k) :=
begin
  sorry,
end

This is I hope true; furthermore it should be an iff, and should also be equivalent to summable (λ ab : α × β, F ab.1 ab.2). Do we have this? Note that some kind of nonnegativity is needed; the grid

1 (-1) 0 0 ...
0   2 (-2) 0 ...
0   0   3  (-3) ...
...

has all row sums and column sums finite therefore convergent, and sum of row sums is 0 but sum of column sums diverges.

[Eric Wieser]

I would imagine a proof goes via a has_sum version of that statement, assuming one can exist

[Vincent Beffara]

Can you map it to docs#measure_theory.integral_integral_swap ? This sounds essentially like Fubini for the counting measure.

[Sebastien Gouezel]

You have docs#ennreal.tsum_comm and all the lemmas that are used in its proof.

[Eric Wieser]

docs#tsum_comm' is fairly close

[Sebastien Gouezel]

(The advantage of working with ennreal is that all sums are well defined there).

[Kevin Buzzard]

Working in ennreal is half of the story. Then for the glue to nnreal I think you need

lemma summable_iff_coe_sum_lt_infty {X : Type*} (f : X → ℝ≥0) :
summable f ↔ ∑' x, (f x : ℝ≥0∞) ≠ ∞ := sorry

and then I think I can simplify some arguments in LTE. Do we have this?

[Kevin Buzzard]

I am have learnt how to dance between nnreal and real because of LTE but now I need to learn a new dance and this is one of the steps.

[Kevin Buzzard]

is this some sort of theorem about with_top of something? For nnreal (but maybe not for real?), summable is registering where some failure occurs in the with_top monad or some such nonsense.

[Kevin Buzzard]

If all this turns out to be nonsense then this isn't an issue for me -- we have sorry-free code in LTE which at some point involves quite a brute force proof that a series converges (as part of a definition of an inverse function), and I'm trying to figure out if there's some conceptual thing behind it.

[Kevin Buzzard]

lemma has_sum_coe {X : Type*} (f : X → ℝ≥0) (a : ℝ≥0) (hfa : has_sum f a) :
  has_sum (λ x, (f x : ℝ≥0∞)) (a : ℝ≥0∞) :=
sorry

seems to help

[Sebastien Gouezel]

We have docs#ennreal.tsum_coe_ne_top_iff_summable and all the lemmas around for the glue you're looking for.

[Sebastien Gouezel]

For instance docs#ennreal.tsum_coe_eq

[Sebastien Gouezel]

or docs#ennreal.has_sum_coe

[Kevin Buzzard]

yeah, I can now move from ennreal to nnreal:

import topology.algebra.infinite_sum
import topology.instances.ennreal

open_locale ennreal

open_locale nnreal

-- don't need it but maybe useful?
lemma ennreal.summable_of_coe_sum_eq {X : Type*} (f g : X → ℝ≥0)
  (h : ∑' x, (f x : ℝ≥0∞) = ∑' x, (g x : ℝ≥0∞)) :
  summable f ↔ summable g :=
by rw [← ennreal.tsum_coe_ne_top_iff_summable, h, ennreal.tsum_coe_ne_top_iff_summable]

lemma ennreal.has_sum_snd_of_has_sum_fst {α β: Type*} (F : α → β → ℝ≥0∞) (s : ℝ≥0∞)
  : has_sum (λ n, ∑' k, F n k) s ↔ has_sum (λ k, ∑' n, F n k) s :=
by rw [ summable.has_sum_iff ennreal.summable, summable.has_sum_iff ennreal.summable,
    ennreal.tsum_comm ]

/-- sum of row sums equals sum of column sums -/
lemma nnreal.summable_snd_of_summable_fst {α β: Type*} (F : α → β → ℝ≥0)
  (h_rows : ∀ n, summable (λ k, F n k)) (h_cols : ∀ k, summable (λ n, F n k))
  (h_col_row : summable (λ k, ∑' n, F n k)) : summable (λ n, ∑' k, F n k) :=
begin
  cases h_col_row with a ha,
  use a,
  rw ← ennreal.has_sum_coe,
  convert_to has_sum (λ n, ∑' k, (F n k : ℝ≥0∞)) a,
  { ext1 n,
    exact ennreal.coe_tsum (h_rows n) },
  { rw ennreal.has_sum_snd_of_has_sum_fst,
    rw ← ennreal.has_sum_coe at ha,
    convert ha,
    ext1 k,
    exact (ennreal.coe_tsum (h_cols k)).symm },
end

[Kevin Buzzard]

I've still got to get to real though!

[Sebastien Gouezel]

You also have glue between nnreal and real, see docs#nnreal.summable_coe_of_nonneg and neighbors.