case h.e'_5
α : Type u_3
E : Type u_2
F : Type ?u.5045186
G : Type ?u.5045189
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Memℒp (f i) p
⊢ ∑ i in s, f i = fun a => ∑ i in s, f i a
α : Type u_3
E : Type u_2
F : Type ?u.5045186
G : Type ?u.5045189
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Memℒp (f i) p
⊢ Memℒp (∑ i in s, f i) p
convert memℒp_finset_sum s hf using 1
case h.e'_5.h
α : Type u_3
E : Type u_2
F : Type ?u.5045186
G : Type ?u.5045189
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Memℒp (f i) p
x : α
⊢ Finset.sum s (fun i => f i) x = ∑ i in s, f i x
case h.e'_5
α : Type u_3
E : Type u_2
F : Type ?u.5045186
G : Type ?u.5045189
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Memℒp (f i) p
⊢ ∑ i in s, f i = fun a => ∑ i in s, f i a
ext x
no goals
case h.e'_5.h
α : Type u_3
E : Type u_2
F : Type ?u.5045186
G : Type ?u.5045189
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Memℒp (f i) p
x : α
⊢ Finset.sum s (fun i => f i) x = ∑ i in s, f i x
simp