𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom 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
𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom s) f
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ ∃ y, y ∈ s ∧ f x ≤ f y
rw [_root_.convexHull_eq.{u, v, 0}] at hx
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom 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
𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom 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
obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom 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
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom 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
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⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
E : Type v
F : Type ?u.65372
β : Type u_1
ι : Type ?u.65378
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 𝕜).toOrderHom 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
exact ⟨p i, hp i hit, Hi⟩