α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ (i : ι), i ∈ s → Memℓp (f i) p
this : DecidableEq ι
⊢ Memℓp (fun a => ∑ i in s, f i a) p
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ (i : ι), i ∈ s → Memℓp (f i) p
⊢ Memℓp (fun a => ∑ i in s, f i a) p
haveI : DecidableEq ι := Classical.decEq _
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ (i : ι), i ∈ s → Memℓp (f i) p
this : DecidableEq ι
⊢ Memℓp (fun a => ∑ i in s, f i a) p
revert hf
case refine'_1
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ (i : ι), i ∈ ∅ → Memℓp (f i) p) → Memℓp (fun a => ∑ i in ∅, f i a) p

case refine'_2
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p) →
        (∀ (i : ι), i ∈ insert a s → Memℓp (f i) p) → Memℓp (fun a_3 => ∑ i in insert a s, f i a_3) p
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p
refine' Finset.induction_on s _ _
no goals
case refine'_1
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ (i : ι), i ∈ ∅ → Memℓp (f i) p) → Memℓp (fun a => ∑ i in ∅, f i a) p
simp only [zero_mem_ℓp', Finset.sum_empty, imp_true_iff]
case refine'_2
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : ¬i ∈ s
ih : (∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p
hf : ∀ (i_1 : ι), i_1 ∈ insert i s → Memℓp (f i_1) p
⊢ Memℓp (fun a => ∑ i in insert i s, f i a) p
case refine'_2
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p) →
        (∀ (i : ι), i ∈ insert a s → Memℓp (f i) p) → Memℓp (fun a_3 => ∑ i in insert a s, f i a_3) p
intro i s his ih hf
case refine'_2
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : ¬i ∈ s
ih : (∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p
hf : ∀ (i_1 : ι), i_1 ∈ insert i s → Memℓp (f i_1) p
⊢ Memℓp (fun a => f i a + ∑ i in s, f i a) p
case refine'_2
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : ¬i ∈ s
ih : (∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p
hf : ∀ (i_1 : ι), i_1 ∈ insert i s → Memℓp (f i_1) p
⊢ Memℓp (fun a => ∑ i in insert i s, f i a) p
simp only [his, Finset.sum_insert, not_false_iff]
no goals
case refine'_2
α : Type u_2
E : α → Type u_3
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_1
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : ¬i ∈ s
ih : (∀ (i : ι), i ∈ s → Memℓp (f i) p) → Memℓp (fun a => ∑ i in s, f i a) p
hf : ∀ (i_1 : ι), i_1 ∈ insert i s → Memℓp (f i_1) p
⊢ Memℓp (fun a => f i a + ∑ i in s, f i a) p
exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))