theorem
MemLp.toLp_sum
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_3}
[DecidableEq ι]
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, MeasureTheory.MemLp (f i) p μ)
:
MeasureTheory.MemLp.toLp (∑ i ∈ s, f i) ⋯ = ∑ i : { x : ι // x ∈ s }, MeasureTheory.MemLp.toLp (f ↑i) ⋯