case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ Memℓp (f + g) 0

case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ Memℓp (f + g) ⊤

case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
⊢ Memℓp (f + g) p
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f + g) p
rcases p.trichotomy with (rfl | rfl | hp)
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
⊢ Summable fun i => ‖(f + g) i‖ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
⊢ Memℓp (f + g) p
apply memℓp_gen
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
⊢ Summable fun i => ‖(f + g) i‖ ^ ENNReal.toReal p
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
⊢ Summable fun i => ‖(f + g) i‖ ^ ENNReal.toReal p
let C : ℝ := if p.toReal < 1 then 1 else (2 : ℝ) ^ (p.toReal - 1)
case inr.inr.hf.refine'_1
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
⊢ ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ ENNReal.toReal p

case inr.inr.hf.refine'_2
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
⊢ ‖(f + g) i‖ ^ ENNReal.toReal p ≤ C * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
⊢ Summable fun i => ‖(f + g) i‖ ^ ENNReal.toReal p
refine'
  summable_of_nonneg_of_le _ (fun i => _) (((hf.summable hp).add (hg.summable hp)).mul_left C)
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ Set.Finite {i | (f + g) i ≠ 0}
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ Memℓp (f + g) 0
apply memℓp_zero
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ i ∈ {i | (f + g) i ≠ 0} → i ∈ {i | f i ≠ 0} ∪ {i | g i ≠ 0}
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ Set.Finite {i | (f + g) i ≠ 0}
refine' (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => _
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ i ∈ {i | (f + g) i ≠ 0} → i ∈ {i | f i ≠ 0} ∪ {i | g i ≠ 0}
simp only [Pi.add_apply, Ne.def, Set.mem_union, Set.mem_setOf_eq]
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ f i = 0 ∧ g i = 0 → f i + g i = 0
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0
contrapose!
case inl.hf.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
hf' : f i = 0
hg' : g i = 0
⊢ f i + g i = 0
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ f i = 0 ∧ g i = 0 → f i + g i = 0
rintro ⟨hf', hg'⟩
no goals
case inl.hf.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
hf' : f i = 0
hg' : g i = 0
⊢ f i + g i = 0
simp [hf', hg']
case inr.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)
case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ Memℓp (f + g) ⊤
apply memℓp_infty
case inr.inl.hf.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)
case inr.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)
obtain ⟨A, hA⟩ := hf.bddAbove
case inr.inl.hf.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)
case inr.inl.hf.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)
obtain ⟨B, hB⟩ := hg.bddAbove
case inr.inl.hf.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ A + B ∈ upperBounds (Set.range fun i => ‖(f + g) i‖)
case inr.inl.hf.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)
refine' ⟨A + B, _⟩
case inr.inl.hf.intro.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
i : α
⊢ (fun i => ‖(f + g) i‖) i ≤ A + B
case inr.inl.hf.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ A + B ∈ upperBounds (Set.range fun i => ‖(f + g) i‖)
rintro a ⟨i, rfl⟩
no goals
case inr.inl.hf.intro.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
i : α
⊢ (fun i => ‖(f + g) i‖) i ≤ A + B
exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))
no goals
case inr.inr.hf.refine'_1
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
⊢ ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ ENNReal.toReal p
exact fun b => Real.rpow_nonneg_of_nonneg (norm_nonneg (f b + g b)) p.toReal
case inr.inr.hf.refine'_2
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤ C * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
case inr.inr.hf.refine'_2
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
⊢ ‖(f + g) i‖ ^ ENNReal.toReal p ≤ C * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
refine' (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans _
case inr.inr.hf.refine'_2
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    (if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)) *
      (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
case inr.inr.hf.refine'_2
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤ C * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
dsimp only
case inr.inr.hf.refine'_2.inl
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
h : ENNReal.toReal p < 1
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤ 1 * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)

case inr.inr.hf.refine'_2.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
h : ¬ENNReal.toReal p < 1
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    2 ^ (ENNReal.toReal p - 1) * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
case inr.inr.hf.refine'_2
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    (if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)) *
      (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
split_ifs with h
no goals
case inr.inr.hf.refine'_2.inl
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
h : ENNReal.toReal p < 1
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤ 1 * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
simpa using NNReal.coe_le_coe.2 (NNReal.rpow_add_le_add_rpow ‖f i‖₊ ‖g i‖₊ hp.le h.le)
case inr.inr.hf.refine'_2.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
h : ¬ENNReal.toReal p < 1
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    2 ^ (ENNReal.toReal p - 1) * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
case inr.inr.hf.refine'_2.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
h : ¬ENNReal.toReal p < 1
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    2 ^ (ENNReal.toReal p - 1) * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
let F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
case inr.inr.hf.refine'_2.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ ENNReal.toReal p
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    2 ^ (ENNReal.toReal p - 1) * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
case inr.inr.hf.refine'_2.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
h : ¬ENNReal.toReal p < 1
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    2 ^ (ENNReal.toReal p - 1) * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
simp only [not_lt] at h
no goals
case inr.inr.hf.refine'_2.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < ENNReal.toReal p
C : ℝ := if ENNReal.toReal p < 1 then 1 else 2 ^ (ENNReal.toReal p - 1)
i : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ ENNReal.toReal p
⊢ (‖f i‖ + ‖g i‖) ^ ENNReal.toReal p ≤
    2 ^ (ENNReal.toReal p - 1) * (‖f i‖ ^ ENNReal.toReal p + ‖g i‖ ^ ENNReal.toReal p)
simpa [Fin.sum_univ_succ] using
  Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg