[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ f (centerMass t w p) ≤ centerMass t w (f ∘ p)
[PROOFSTEP]
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} := fun i hi => ⟨hmem i hi, le_rfl⟩
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
hmem' : ∀ (i : ι), i ∈ t → (p i, (f ∘ p) i) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
⊢ f (centerMass t w p) ≤ centerMass t w (f ∘ p)
[PROOFSTEP]
convert (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2
[GOAL]
case h.e'_3.h.e'_1
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
hmem' : ∀ (i : ι), i ∈ t → (p i, (f ∘ p) i) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
⊢ centerMass t w p = (centerMass t (fun i => w i) fun i => (p i, (f ∘ p) i)).fst
[PROOFSTEP]
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]
[GOAL]
case h.e'_4
𝕜 : Type u_3
E : Type u_2
F : Type ?u.962
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : 0 < ∑ i in t, w i
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
hmem' : ∀ (i : ι), i ∈ t → (p i, (f ∘ p) i) ∈ {p | p.fst ∈ s ∧ f p.fst ≤ p.snd}
⊢ centerMass t w (f ∘ p) = (centerMass t (fun i => w i) fun i => (p i, (f ∘ p) i)).snd
[PROOFSTEP]
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.21511
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : ∑ i in t, w i = 1
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ f (∑ i in t, w i • p i) ≤ ∑ i in t, w i • f (p i)
[PROOFSTEP]
simpa only [centerMass, h₁, inv_one, one_smul] using hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem
[GOAL]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
hx : x ∈ ↑(convexHull 𝕜) ↑s
⊢ f x ≤ sup' s (_ : Finset.Nonempty s) f
[PROOFSTEP]
obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convexHull.1 hx
[GOAL]
case intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜) ↑s
⊢ f (centerMass s w _root_.id) ≤ sup' s (_ : Finset.Nonempty s) f
[PROOFSTEP]
exact (hf.map_centerMass_le hw₀ (by positivity) <| subset_convexHull _ _).trans (centerMass_le_sup hw₀ <| by positivity)
[GOAL]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜) ↑s
⊢ 0 < ∑ i in s, w i
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.35782
β : Type u_2
ι : Type ?u.35788
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜) ↑s
⊢ 0 < ∑ i in s, w i
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ ∃ i, i ∈ t ∧ f (centerMass t w p) ≤ f (p i)
[PROOFSTEP]
set y := t.centerMass w p
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
obtain ⟨i, hi, hfi⟩ : ∃ i ∈ t.filter fun i => w i ≠ 0, w i • f y ≤ w i • (f ∘ p) i
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ ∃ i, i ∈ filter (fun i => w i ≠ 0) t ∧ w i • f y ≤ w i • (f ∘ p) i
case intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) t
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) t
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
rw [mem_filter] at hi 
[GOAL]
case intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
i : ι
hi : i ∈ t ∧ w i ≠ 0
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i, i ∈ t ∧ f y ≤ f (p i)
[PROOFSTEP]
exact ⟨i, hi.1, (smul_le_smul_iff_of_pos <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ ∃ i, i ∈ filter (fun i => w i ≠ 0) t ∧ w i • f y ≤ w i • (f ∘ p) i
[PROOFSTEP]
have hw' : (0 : 𝕜) < ∑ i in filter (fun i => w i ≠ 0) t, w i := by rwa [sum_filter_ne_zero]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
⊢ 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
[PROOFSTEP]
rwa [sum_filter_ne_zero]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
hw' : 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
⊢ ∃ i, i ∈ filter (fun i => w i ≠ 0) t ∧ w i • f y ≤ w i • (f ∘ p) i
[PROOFSTEP]
refine' exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') _
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
hw' : 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
⊢ ∑ i in filter (fun i => w i ≠ 0) t, w i • f y ≤ ∑ i in filter (fun i => w i ≠ 0) t, w i • (f ∘ p) i
[PROOFSTEP]
rw [← sum_smul, ← smul_le_smul_iff_of_pos (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ← Finset.centerMass,
  Finset.centerMass_filter_ne_zero]
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.90866
β : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
h : ConvexOn 𝕜 s f
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : 0 < ∑ i in t, w i
hp : ∀ (i : ι), i ∈ t → p i ∈ s
y : E := centerMass t w p
hw' : 0 < ∑ i in filter (fun i => w i ≠ 0) t, w i
⊢ f y ≤ centerMass t (fun i => w i) fun i => (f ∘ p) i
[PROOFSTEP]
exact h.map_centerMass_le hw₀ hw₁ hp
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x✝ : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ ∃ y, y ∈ s ∧ f x ≤ f y
[PROOFSTEP]
rw [_root_.convexHull_eq] at hx 
[GOAL]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x✝ : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
x : E
hx : x ∈ {x | ∃ ι t w z x_1 x_2 x_3, centerMass t w z = x}
⊢ ∃ y, y ∈ s ∧ f x ≤ f y
[PROOFSTEP]
obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t✝ : Finset ι
w✝ : ι → 𝕜
p✝ : ι → E
x : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ (i : α), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hp : ∀ (i : α), i ∈ t → p i ∈ s
⊢ ∃ y, y ∈ s ∧ f (centerMass t w p) ≤ f y
[PROOFSTEP]
rcases hf.exists_ge_of_centerMass hw₀ (hw₁.symm ▸ zero_lt_one) fun i hi => subset_convexHull 𝕜 s (hp i hi) with
  ⟨i, hit, Hi⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.105120
β : Type u_1
ι : Type ?u.105126
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t✝ : Finset ι
w✝ : ι → 𝕜
p✝ : ι → E
x : E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ (i : α), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hp : ∀ (i : α), i ∈ t → p i ∈ s
i : α
hit : i ∈ t
Hi : f (centerMass t (fun i => w i) fun i => p i) ≤ f (p i)
⊢ ∃ y, y ∈ s ∧ f (centerMass t w p) ≤ f y
[PROOFSTEP]
exact ⟨p i, hp i hit, Hi⟩
