integral sum measure

Stream: Is there code for X?

[Alex Kontorovich]

Is this true? (There's a version for lintegral but how to prove this for Bochner?) (Perhaps @Yury G. Kudryashov or @Sebastien Gouezel know immediately?) Came up in discussion with @Heather Macbeth

import measure_theory.integral.bochner

open measure_theory topological_space

variables {α E : Type*} [measurable_space α] [normed_group E] {s t : set α} {μ : measure α} [measurable_space E] [normed_space ℝ E] [borel_space E] [complete_space E] [second_countable_topology E]

theorem integral_sum_measure {ι : Type*} (f : α → E) (μ : ι → measure α) (hf : integrable f (measure.sum μ)) :
∫ (a : α), f a ∂measure.sum μ = ∑' (i : ι), ∫ (a : α), f a ∂μ i :=
begin
  refine integrable.induction _ _ _ _ _ hf,

  repeat {sorry},

  -- FYI This is how `lintegral_sum_measure` is proved:

  -- simp only [integral, supr_subtype', simple_func.integral_sum, ennreal.tsum_eq_supr_sum],
  -- rw [supr_comm],
  -- congr, funext s,
  -- induction s using finset.induction_on with i s hi hs, { apply bot_unique, simp },
  -- simp only [finset.sum_insert hi, ← hs],
  -- refine (ennreal.supr_add_supr _).symm,
  -- intros φ ψ,
  -- exact ⟨⟨φ ⊔ ψ, λ x, sup_le (φ.2 x) (ψ.2 x)⟩,
  --   add_le_add (simple_func.lintegral_mono le_sup_left le_rfl)
  --     (finset.sum_le_sum $ λ j hj, simple_func.lintegral_mono le_sup_right le_rfl)⟩
end

[Yury G. Kudryashov]

I'll try to prove it.

[Yury G. Kudryashov]

I have it (and several supporting lemmas). I'll make a PR later tonight.

[Yury G. Kudryashov]

#12005

[Heather Macbeth]

Thanks, @Yury G. Kudryashov !

[Yury G. Kudryashov]

I wonder if there is a version that implies docs#measure_theory.tendsto_set_integral_of_monotone