𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) ↔
    Convex 𝕜 s ∧
      Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
rw [convexOn_iff_forall_pos]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) ↔
    Convex 𝕜 s ∧
      Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
refine'
  and_congr_right'
    ⟨fun h x hx y hy _ a b ha hb hab => h hx hy ha hb hab, fun h x hx y hy a b ha hb hab => _⟩
case inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy : x ∈ s
⊢ f (a • x + b • x) ≤ a • f x + b • f x

case inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x ≠ y
⊢ f (a • x + b • y) ≤ a • f x + b • f y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y
obtain rfl | hxy := eq_or_ne x y
no goals
case inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x ≠ y
⊢ f (a • x + b • y) ≤ a • f x + b • f y
exact h hx hy hxy ha hb hab
no goals
case inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.162921
α : Type ?u.162924
β : Type u_3
ι : Type ?u.162930
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy : x ∈ s
⊢ f (a • x + b • x) ≤ a • f x + b • f x
rw [Convex.combo_self hab, Convex.combo_self hab]