case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i => g i ^ p
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
⊢ (Summable fun i => ((fun i => ↑(f i)) i + g i) ^ p) ∧
    (∑' (i : ι), ((fun i => ↑(f i)) i + g i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i => f i ^ p
hg_sum : Summable fun i => g i ^ p
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
lift f to ι → ℝ≥0 using hf
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i => (fun i => ↑(g i)) i ^ p
⊢ (Summable fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) ∧
    (∑' (i : ι), ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), (fun i => ↑(g i)) i ^ p) ^ (1 / p)
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i => g i ^ p
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
⊢ (Summable fun i => ((fun i => ↑(f i)) i + g i) ^ p) ∧
    (∑' (i : ι), ((fun i => ↑(f i)) i + g i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
lift g to ι → ℝ≥0 using hg
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
f g : ι → ℝ≥0
hp : 1 ≤ p
hf_sum : Summable fun a => f a ^ p
hg_sum : Summable fun a => g a ^ p
⊢ (Summable fun a => (f a + g a) ^ p) ∧
    (∑' (a : ι), (f a + g a) ^ p) ^ (1 / p) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) + (∑' (a : ι), g a ^ p) ^ (1 / p)
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i => (fun i => ↑(g i)) i ^ p
⊢ (Summable fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) ∧
    (∑' (i : ι), ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), (fun i => ↑(g i)) i ^ p) ^ (1 / p)
norm_cast0 at *
no goals
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
f g : ι → ℝ≥0
hp : 1 ≤ p
hf_sum : Summable fun a => f a ^ p
hg_sum : Summable fun a => g a ^ p
⊢ (Summable fun a => (f a + g a) ^ p) ∧
    (∑' (a : ι), (f a + g a) ^ p) ^ (1 / p) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) + (∑' (a : ι), g a ^ p) ^ (1 / p)
exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum