ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this :
  ↑((∑ i in s,
          ((fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i +
              (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i) ^
            p) ^
        (1 / p)) ≤
    ↑((∑ i in s, (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i ^ p) ^ (1 / p) +
        (∑ i in s, (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i ^ p) ^ (1 / p))
⊢ (∑ i in s, abs (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) + (∑ i in s, abs (g i) ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, abs (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) + (∑ i in s, abs (g i) ^ p) ^ (1 / p)
have :=
  NNReal.coe_le_coe.2
    (NNReal.Lp_add_le s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) hp)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this :
  (∑ x in s, (abs (f x) + abs (g x)) ^ p) ^ (1 / p) ≤
    (∑ x in s, abs (f x) ^ p) ^ (1 / p) + (∑ x in s, abs (g x) ^ p) ^ (1 / p)
⊢ (∑ i in s, abs (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) + (∑ i in s, abs (g i) ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this :
  ↑((∑ i in s,
          ((fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i +
              (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i) ^
            p) ^
        (1 / p)) ≤
    ↑((∑ i in s, (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i ^ p) ^ (1 / p) +
        (∑ i in s, (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i ^ p) ^ (1 / p))
⊢ (∑ i in s, abs (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) + (∑ i in s, abs (g i) ^ p) ^ (1 / p)
push_cast at this
no goals
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this :
  (∑ x in s, (abs (f x) + abs (g x)) ^ p) ^ (1 / p) ≤
    (∑ x in s, abs (f x) ^ p) ^ (1 / p) + (∑ x in s, abs (g x) ^ p) ^ (1 / p)
⊢ (∑ i in s, abs (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) + (∑ i in s, abs (g i) ^ p) ^ (1 / p)
refine' le_trans (rpow_le_rpow _ (sum_le_sum fun i _ => _) _) this <;>
  simp [sum_nonneg, rpow_nonneg_of_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add,
    rpow_le_rpow]