𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
set y := t.centerMass w p
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
obtain ⟨i, hi, hfi⟩ : ∃ i ∈ t.filter fun i => w i ≠ 0, w i • f y ≤ w i • (f ∘ p) i
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)

𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
rotate_left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
have hw' : (0 : 𝕜) < ∑ i in filter (fun i => w i ≠ 0) t, w i := by rwa [sum_filter_ne_zero]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
refine' exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') _
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
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]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
exact h.map_centerMass_le hw₀ hw₁ hp
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
rw [mem_filter] at hi
no goals
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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)
exact ⟨i, hi.1, (smul_le_smul_iff_of_pos <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51124
β : Type u_3
ι : 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
rwa [sum_filter_ne_zero]