ι : 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) ^ p) ≤
    ↑(↑(card s) ^ (p - 1) * ∑ i in s, (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i ^ p)
⊢ (∑ i in s, abs (f i)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, abs (f i) ^ p
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, abs (f i)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, abs (f i) ^ p
have :=
  NNReal.coe_le_coe.2
    (NNReal.rpow_sum_le_const_mul_sum_rpow s (fun i => ⟨_, abs_nonneg (f i)⟩) hp)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this : (∑ x in s, abs (f x)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ x in s, abs (f x) ^ p
⊢ (∑ i in s, abs (f i)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, abs (f i) ^ 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) ^ p) ≤
    ↑(↑(card s) ^ (p - 1) * ∑ i in s, (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i ^ p)
⊢ (∑ i in s, abs (f i)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, abs (f i) ^ 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)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ x in s, abs (f x) ^ p
⊢ (∑ i in s, abs (f i)) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, abs (f i) ^ p
exact this