case pos
ι : 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
A : ∃ i, i ∈ s ∧ z i = 0 ∧ w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i

case neg
ι : 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
A : ¬∃ i, i ∈ s ∧ z i = 0 ∧ w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ 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
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
by_cases A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
case pos
ι : 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
A : ∃ i, i ∈ s ∧ z i = 0 ∧ w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
rcases A with ⟨i, his, hzi, hwi⟩
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ≤ ∑ i in s, w i * z i

case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
rw [prod_eq_zero his]
no goals
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ≤ ∑ i in s, w i * z i
exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ^ w i = 0
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
rw [hzi]
no goals
case pos.intro.intro.intro
ι : 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ^ w i = 0
exact zero_rpow hwi
case neg
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
case neg
ι : 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
A : ¬∃ i, i ∈ s ∧ z i = 0 ∧ w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
simp only [not_exists, not_and, Ne.def, Classical.not_not] at A
case neg
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : exp (∑ i in s, w i • log (z i)) ≤ ∑ i in s, w i • exp (log (z i))
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
case neg
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
case h.e'_3
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
⊢ z i ^ w i = exp (log (z i) * w i)

case h.e'_4
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
⊢ w i * z i = w i * exp (log (z i))
case neg
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
convert this using 1 <;> [apply prod_congr rfl;apply sum_congr rfl] <;> intro i hi
case h.e'_3.inl
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ z i ^ w i = exp (log (z i) * w i)

case h.e'_3.inr
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = exp (log (z i) * w i)
case h.e'_3
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
⊢ z i ^ w i = exp (log (z i) * w i)
cases' eq_or_lt_of_le (hz i hi) with hz hz
no goals
case h.e'_3.inl
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ z i ^ w i = exp (log (z i) * w i)
simp [A i hi hz.symm]
no goals
case h.e'_3.inr
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = exp (log (z i) * w i)
exact rpow_def_of_pos hz _
case h.e'_4.inl
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ w i * z i = w i * exp (log (z i))

case h.e'_4.inr
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * exp (log (z i))
case h.e'_4
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
⊢ w i * z i = w i * exp (log (z i))
cases' eq_or_lt_of_le (hz i hi) with hz hz
no goals
case h.e'_4.inl
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ w i * z i = w i * exp (log (z i))
simp [A i hi hz.symm]
no goals
case h.e'_4.inr
ι : 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
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * exp (log (z i))
rw [exp_log hz]