Interchanging sums and integrals

Stream: Is there code for X?

[David Loeffler]

Is the following in mathlib?

Let $\Omega$ be a measure space, and $(f_i)_{i \in \mathbb{N}}$ functions on $\Omega$ (valued in a Banach space). Suppose $\sum_{i \in \mathbb{N}} f_i(x)$ converges almost everywhere, and the sum $\sum_i \int_{\Omega} \|f_i(x)\|\, \mathrm{d}x < \infty$. Then $\int_\Omega (\sum_i f_i(x)) \mathrm{d}x = \sum_i \int_\Omega f_i(x) \, \mathrm{d}x$.

It can be deduced from the more general Lebesgue dominated convergence theorem (docs#hasSum_integral_of_dominated_convergence) but the deduction isn't totally straightforward, so I'm wondering if we have this as a separate lemma.

[Eric Wieser]

I needed but couldn't find this in #9487

[David Loeffler]

Eric Wieser said:

I needed but couldn't find this in #9487

That sounds like a vote in favour of adding it. The statement I have formalised is

hasSum_integral_of_summable_norm {E ι α : Type*} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace α]
  {μ : Measure α} [Countable ι] (F : ι → α → E) (hF_int : ∀ (i : ι), Integrable (F i))
  (hF_sum : ∀ᵐ (a : α) ∂μ, Summable fun x ↦ ‖F x a‖) (hF_sum' : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ) :
  HasSum (fun n ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ) := sorry

Does that fit what you needed for #9487?

[David Loeffler]

Hang on, some version of this is there already: the innocuously named docs#integral_tsum. I'm still going to PR this version because I think it's more user-friendly to have formulations which don't explicitly involve ENNReal, lintegral etc.

[Igor Khavkine]

In principle, one could also cobble this result together from Fubini's theorem in docs#MeasureTheory.integral_integral_swap and this missing counter-part to docs#MeasureTheory.lintegral_count

import Mathlib

open BigOperators ENNReal MeasureTheory
open Measure

theorem integral_count {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
      [Countable α] [MeasurableSingletonClass α]
      [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
      (f : α → F) (hf : Integrable f count) :
    ∫ a, f a ∂count = ∑' a, f a := by
  convert integral_countable' hf
  rw [count_singleton]
  simp only [one_toReal, one_smul]

[Sébastien Gouëzel]

@David Loeffler, you shouldn't need hF_sum, it can de deduced from the other assumptions. (If it were not summable ae, then the sum of the integrals would be infinite, which contradicts hF_sum').

[David Loeffler]

Yes, you're right! I have posted a PR #10614 (without the pointwise summability assumption).