case hp_pos
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
have hp_pos : 0 < p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
case hp_pos
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
positivity
case hp_nonneg
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p

ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
have hp_nonneg : 0 ≤ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
case hp_nonneg
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p

ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
positivity
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
have hp_not_neg : ¬p < 0 := by simp [hp_nonneg]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
have h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤) := by
  simp [ENNReal.mul_eq_top, hp_pos, hp_nonneg, hp_not_neg]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p = ⊤ → ∑ i in s, w i * z i ^ p = ⊤

case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≠ ⊤ →
    ∑ i in s, w i * z i ^ p ≠ ⊤ →
      ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
refine' le_of_top_imp_top_of_toNNReal_le _ _
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ ¬p < 0
simp [hp_nonneg]
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
simp [ENNReal.mul_eq_top, hp_pos, hp_nonneg, hp_not_neg]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p → ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p = ⊤ → ∑ i in s, w i * z i ^ p = ⊤
rw [rpow_eq_top_iff, sum_eq_top_iff, sum_eq_top_iff]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p → ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
intro h
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
simp only [and_false_iff, hp_not_neg, false_or_iff] at h
case refine'_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
rcases h.left with ⟨a, H, ha⟩
case refine'_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ w a * z a ^ p = ⊤
case refine'_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
use a, H
no goals
case refine'_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ w a * z a ^ p = ⊤
rwa [← h_top_iff_rpow_top a H]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≠ ⊤ →
    ∑ i in s, w i * z i ^ p ≠ ⊤ →
      ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
intro h_top_rpow_sum _
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
  haveI h_top_sum : (∑ i : ι in s, w i * z i) ≠ ⊤ := by
    intro h
    rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
    exact h_top_rpow_sum rfl
  fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ := by
  intro i hi
  specialize h_top i hi
  rwa [Ne.def, ← h_top_iff_rpow_top i hi]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ (∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x)) ^ p ≤
    ∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x) ^ p
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
simp_rw [toNNReal_sum h_top_rpow, ← toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul, ←
  toNNReal_rpow]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ (∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x)) ^ p ≤
    ∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x) ^ p
refine'
  NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal)
    (fun i => (z i).toNNReal) _ hp
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
h_sum_nnreal : ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
have h_sum_nnreal : (∑ i in s, w i) = ↑(∑ i in s, (w i).toNNReal) := by
  rw [coe_finset_sum]
  refine' sum_congr rfl fun i hi => (coe_toNNReal _).symm
  refine' (lt_top_of_sum_ne_top _ hi).ne
  exact hw'.symm ▸ ENNReal.one_ne_top
no goals
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
h_sum_nnreal : ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
rwa [← coe_eq_coe, ← h_sum_nnreal]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ∑ i in s, w i * z i ≠ ⊤
intro h
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : ⊤ ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : ⊤ ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
exact h_top_rpow_sum rfl
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ⊤
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
intro i hi
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ⊤
⊢ w i * z i ^ p ≠ ⊤
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ⊤
specialize h_top i hi
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ⊤
⊢ w i * z i ^ p ≠ ⊤
rwa [Ne.def, ← h_top_iff_rpow_top i hi]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ∑ a in s, ↑(ENNReal.toNNReal (w a))
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
rw [coe_finset_sum]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i ≠ ⊤
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ∑ a in s, ↑(ENNReal.toNNReal (w a))
refine' sum_congr rfl fun i hi => (coe_toNNReal _).symm
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ ∑ x in s, w x ≠ ⊤
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i ≠ ⊤
refine' (lt_top_of_sum_ne_top _ hi).ne
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ ∑ x in s, w x ≠ ⊤
exact hw'.symm ▸ ENNReal.one_ne_top