𝕜 : Type u_1
E : Type u_2
F : Type ?u.962
β : Type u_3
ι : 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)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.962
β : Type u_3
ι : 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)
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⟩
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.962
β : Type u_3
ι : 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)
convert(hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2 <;>
  simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]