α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
⊢ ‖f‖ ^ ENNReal.toReal p - ‖f - ∑ i in s, lp.single p i (↑f i)‖ ^ ENNReal.toReal p = ∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p
refine' ((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i in s, lp.single p i (f i)))).unique _
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
let F : α → ℝ := fun i => ‖f i‖ ^ p.toReal - ‖(f - ∑ i in s, lp.single p i (f i)) i‖ ^ p.toReal
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
have hF : ∀ (i) (_ : i ∉ s), F i = 0 := by
  intro i hi
  suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
    simpa only [coeFn_sum, lp.single_apply, coeFn_sub, Pi.sub_apply, Finset.sum_apply,
      Finset.sum_dite_eq] using this
  simp only [if_neg hi, sub_zero, sub_self]
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
hF' : ∀ (i : α), i ∈ s → F i = ‖↑f i‖ ^ ENNReal.toReal p
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
have hF' : ∀ i ∈ s, F i = ‖f i‖ ^ p.toReal := by
  intro i hi
  simp only [coeFn_sum, lp.single_apply, if_pos hi, sub_self, eq_self_iff_true, coeFn_sub,
    Pi.sub_apply, Finset.sum_apply, Finset.sum_dite_eq, sub_eq_self]
  simp [Real.zero_rpow hp.ne']
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
hF' : ∀ (i : α), i ∈ s → F i = ‖↑f i‖ ^ ENNReal.toReal p
this : HasSum F (∑ i in s, F i)
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
hF' : ∀ (i : α), i ∈ s → F i = ‖↑f i‖ ^ ENNReal.toReal p
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
have : HasSum F (∑ i in s, F i) := hasSum_sum_of_ne_finset_zero hF
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
hF' : ∀ (i : α), i ∈ s → F i = ‖↑f i‖ ^ ENNReal.toReal p
this : HasSum F (∑ i in s, F i)
⊢ HasSum (fun b => ‖↑f b‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) b‖ ^ ENNReal.toReal p)
    (∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p)
rwa [Finset.sum_congr rfl hF'] at this
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
i : α
hi : ¬i ∈ s
⊢ F i = 0
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
⊢ ∀ (i : α), ¬i ∈ s → F i = 0
intro i hi
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
i : α
hi : ¬i ∈ s
⊢ ‖↑f i‖ ^ ENNReal.toReal p - ‖↑f i - if i ∈ s then ↑f i else 0‖ ^ ENNReal.toReal p = 0
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
i : α
hi : ¬i ∈ s
⊢ F i = 0
suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
  simpa only [coeFn_sum, lp.single_apply, coeFn_sub, Pi.sub_apply, Finset.sum_apply,
    Finset.sum_dite_eq] using this
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
i : α
hi : ¬i ∈ s
⊢ ‖↑f i‖ ^ ENNReal.toReal p - ‖↑f i - if i ∈ s then ↑f i else 0‖ ^ ENNReal.toReal p = 0
simp only [if_neg hi, sub_zero, sub_self]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
i : α
hi : ¬i ∈ s
this : ‖↑f i‖ ^ ENNReal.toReal p - ‖↑f i - if i ∈ s then ↑f i else 0‖ ^ ENNReal.toReal p = 0
⊢ F i = 0
simpa only [coeFn_sum, lp.single_apply, coeFn_sub, Pi.sub_apply, Finset.sum_apply,
  Finset.sum_dite_eq] using this
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
i : α
hi : i ∈ s
⊢ F i = ‖↑f i‖ ^ ENNReal.toReal p
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
⊢ ∀ (i : α), i ∈ s → F i = ‖↑f i‖ ^ ENNReal.toReal p
intro i hi
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
i : α
hi : i ∈ s
⊢ ‖0‖ ^ ENNReal.toReal p = 0
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
i : α
hi : i ∈ s
⊢ F i = ‖↑f i‖ ^ ENNReal.toReal p
simp only [coeFn_sum, lp.single_apply, if_pos hi, sub_self, eq_self_iff_true, coeFn_sub,
  Pi.sub_apply, Finset.sum_apply, Finset.sum_dite_eq, sub_eq_self]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type ?u.935439
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
s : Finset α
F : α → ℝ := fun i => ‖↑f i‖ ^ ENNReal.toReal p - ‖↑(f - ∑ i in s, lp.single p i (↑f i)) i‖ ^ ENNReal.toReal p
hF : ∀ (i : α), ¬i ∈ s → F i = 0
i : α
hi : i ∈ s
⊢ ‖0‖ ^ ENNReal.toReal p = 0
simp [Real.zero_rpow hp.ne']