ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
have : 0 < p := by positivity
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p

case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p

case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
no goals
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
all_goals
  apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
  intro i hi
  apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ 0 < p
positivity
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i ^ p
intro i hi
no goals
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]