[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
have hxz := hxy.trans hyz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxz : x < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
rw [← sub_pos] at hxy hxz hyz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
suffices f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
  by
  ring_nf at this ⊢
  linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
this : f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
ring_nf at this ⊢
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
this : f y * (y - x)⁻¹ + f y * (-y + z)⁻¹ ≤ (y - x)⁻¹ * f x + (-y + z)⁻¹ * f z
⊢ f y * (y - x)⁻¹ - (y - x)⁻¹ * f x ≤ -(f y * (-y + z)⁻¹) + (-y + z)⁻¹ * f z
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
set a := (z - y) / (z - x)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
set b := (y - x) / (z - x)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
have hy : a • x + b • z = y := by
  field_simp
  rw [div_eq_iff] <;> [ring; linarith]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ a • x + b • z = y
[PROOFSTEP]
field_simp
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ ((z - y) * x + (y - x) * z) / (z - x) = y
[PROOFSTEP]
rw [div_eq_iff] <;> [ring; linarith]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ ((z - y) * x + (y - x) * z) / (z - x) = y
[PROOFSTEP]
rw [div_eq_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ (z - y) * x + (y - x) * z = y * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ z - x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
have key :=
  hf.2 hx hz (show 0 ≤ a by apply div_nonneg <;> linarith) (show 0 ≤ b by apply div_nonneg <;> linarith)
    (show a + b = 1 by
      field_simp
      rw [div_eq_iff] <;> [ring; linarith])
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ 0 ≤ a
[PROOFSTEP]
apply div_nonneg
[GOAL]
case ha
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ 0 ≤ z - y
[PROOFSTEP]
linarith
[GOAL]
case hb
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ 0 ≤ z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ 0 ≤ b
[PROOFSTEP]
apply div_nonneg
[GOAL]
case ha
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ 0 ≤ y - x
[PROOFSTEP]
linarith
[GOAL]
case hb
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ 0 ≤ z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ a + b = 1
[PROOFSTEP]
field_simp
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ (z - x) / (z - x) = 1
[PROOFSTEP]
rw [div_eq_iff] <;> [ring; linarith]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ (z - x) / (z - x) = 1
[PROOFSTEP]
rw [div_eq_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ z - x = 1 * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ z - x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f (a • x + b • z) ≤ a • f x + b • f z
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
rw [hy] at key
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y ≤ a • f x + b • f z
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
replace key := mul_le_mul_of_nonneg_left key hxz.le
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : (z - x) * f y ≤ (z - x) * (a • f x + b • f z)
⊢ f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
[PROOFSTEP]
field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _] at key ⊢
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z
⊢ (f y * (z - y) + f y * (y - x)) / ((y - x) * (z - y)) ≤ (f x * (z - y) + f z * (y - x)) / ((y - x) * (z - y))
[PROOFSTEP]
rw [div_le_div_right]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z
⊢ f y * (z - y) + f y * (y - x) ≤ f x * (z - y) + f z * (y - x)
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z
⊢ 0 < (y - x) * (z - y)
[PROOFSTEP]
nlinarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
[PROOFSTEP]
have := neg_le_neg (ConvexOn.slope_mono_adjacent hf.neg hx hz hxy hyz)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : -(((-f) z - (-f) y) / (z - y)) ≤ -(((-f) y - (-f) x) / (y - x))
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
[PROOFSTEP]
simp only [Pi.neg_apply, ← neg_div, neg_sub', neg_neg] at this
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
[PROOFSTEP]
exact this
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
[PROOFSTEP]
have hxz := hxy.trans hyz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxz : x < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
[PROOFSTEP]
have hxz' := hxz.ne
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxz : x < z
hxz' : x ≠ z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
[PROOFSTEP]
rw [← sub_pos] at hxy hxz hyz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
[PROOFSTEP]
suffices f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
  by
  ring_nf at this ⊢
  linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
this : f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
[PROOFSTEP]
ring_nf at this ⊢
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
this : f y * (y - x)⁻¹ + f y * (-y + z)⁻¹ < (y - x)⁻¹ * f x + (-y + z)⁻¹ * f z
⊢ f y * (y - x)⁻¹ - (y - x)⁻¹ * f x < -(f y * (-y + z)⁻¹) + (-y + z)⁻¹ * f z
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
set a := (z - y) / (z - x)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
set b := (y - x) / (z - x)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
have hy : a • x + b • z = y := by
  field_simp
  rw [div_eq_iff] <;> [ring; linarith]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ a • x + b • z = y
[PROOFSTEP]
field_simp
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ ((z - y) * x + (y - x) * z) / (z - x) = y
[PROOFSTEP]
rw [div_eq_iff] <;> [ring; linarith]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ ((z - y) * x + (y - x) * z) / (z - x) = y
[PROOFSTEP]
rw [div_eq_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ (z - y) * x + (y - x) * z = y * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
⊢ z - x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
have key :=
  hf.2 hx hz hxz' (div_pos hyz hxz) (div_pos hxy hxz)
    (show a + b = 1 by
      field_simp
      rw [div_eq_iff] <;> [ring; linarith])
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ a + b = 1
[PROOFSTEP]
field_simp
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ (z - x) / (z - x) = 1
[PROOFSTEP]
rw [div_eq_iff] <;> [ring; linarith]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ (z - x) / (z - x) = 1
[PROOFSTEP]
rw [div_eq_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ z - x = 1 * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
⊢ z - x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) < ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
rw [hy] at key
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y < ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
replace key := mul_lt_mul_of_pos_left key hxz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : (z - x) * f y < (z - x) * (((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z)
⊢ f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
[PROOFSTEP]
field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _] at key ⊢
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) < (z - y) * f x + (y - x) * f z
⊢ (f y * (z - y) + f y * (y - x)) / ((y - x) * (z - y)) < (f x * (z - y) + f z * (y - x)) / ((y - x) * (z - y))
[PROOFSTEP]
rw [div_lt_div_right]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) < (z - y) * f x + (y - x) * f z
⊢ f y * (z - y) + f y * (y - x) < f x * (z - y) + f z * (y - x)
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy✝ : x < y
hxy : 0 < y - x
hyz✝ : y < z
hyz : 0 < z - y
hxz✝ : x < z
hxz : 0 < z - x
hxz' : x ≠ z
a : 𝕜 := (z - y) / (z - x)
b : 𝕜 := (y - x) / (z - x)
hy : a • x + b • z = y
key : f y * (z - x) < (z - y) * f x + (y - x) * f z
⊢ 0 < (y - x) * (z - y)
[PROOFSTEP]
nlinarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)
[PROOFSTEP]
have := neg_lt_neg (StrictConvexOn.slope_strict_mono_adjacent hf.neg hx hz hxy hyz)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : -(((-f) z - (-f) y) / (z - y)) < -(((-f) y - (-f) x) / (y - x))
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)
[PROOFSTEP]
simp only [Pi.neg_apply, ← neg_div, neg_sub', neg_neg] at this
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)
[PROOFSTEP]
exact this
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
let y := a * x + b * z
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
have hxy : x < y := by
  rw [← one_mul x, ← hab, add_mul]
  exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ x < y
[PROOFSTEP]
rw [← one_mul x, ← hab, add_mul]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ a * x + b * x < y
[PROOFSTEP]
exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
have hyz : y < z := by
  rw [← one_mul z, ← hab, add_mul]
  exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < z
[PROOFSTEP]
rw [← one_mul z, ← hab, add_mul]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < a * z + b * z
[PROOFSTEP]
exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
have : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x) :=
  (div_le_div_iff (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
have hxz : 0 < z - x := sub_pos.2 (hxy.trans hyz)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
have ha : (z - y) / (z - x) = a := by
  rw [eq_comm, ← sub_eq_iff_eq_add'] at hab
  simp_rw [div_eq_iff hxz.ne', ← hab]
  ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ (z - y) / (z - x) = a
[PROOFSTEP]
rw [eq_comm, ← sub_eq_iff_eq_add'] at hab
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 1 - a = b
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ (z - y) / (z - x) = a
[PROOFSTEP]
simp_rw [div_eq_iff hxz.ne', ← hab]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 1 - a = b
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ z - (a * x + (1 - a) * z) = a * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
have hb : (y - x) / (z - x) = b := by
  rw [eq_comm, ← sub_eq_iff_eq_add] at hab
  simp_rw [div_eq_iff hxz.ne', ← hab]
  ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b
[PROOFSTEP]
rw [eq_comm, ← sub_eq_iff_eq_add] at hab
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b
[PROOFSTEP]
simp_rw [div_eq_iff hxz.ne', ← hab]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (1 - b) * x + b * z - x = b * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb✝ : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
hb : (y - x) / (z - x) = b
⊢ f (a • x + b • z) ≤ a • f x + b • f z
[PROOFSTEP]
rwa [sub_mul, sub_mul, sub_le_iff_le_add', ← add_sub_assoc, le_sub_iff_add_le, ← mul_add, sub_add_sub_cancel, ←
  le_div_iff hxz, add_div, mul_div_assoc, mul_div_assoc, mul_comm (f x), mul_comm (f z), ha, hb] at this
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConcaveOn 𝕜 s f
[PROOFSTEP]
rw [← neg_convexOn_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConvexOn 𝕜 s (-f)
[PROOFSTEP]
refine' convexOn_of_slope_mono_adjacent hs fun hx hz hxy hyz => _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ ((-f) y✝ - (-f) x✝) / (y✝ - x✝) ≤ ((-f) z✝ - (-f) y✝) / (z✝ - y✝)
[PROOFSTEP]
rw [← neg_le_neg_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ -(((-f) z✝ - (-f) y✝) / (z✝ - y✝)) ≤ -(((-f) y✝ - (-f) x✝) / (y✝ - x✝))
[PROOFSTEP]
simp_rw [← neg_div, neg_sub, Pi.neg_apply, neg_sub_neg]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ (f z✝ - f y✝) / (z✝ - y✝) ≤ (f y✝ - f x✝) / (y✝ - x✝)
[PROOFSTEP]
exact hf hx hz hxy hyz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
let y := a * x + b * z
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
have hxy : x < y := by
  rw [← one_mul x, ← hab, add_mul]
  exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ x < y
[PROOFSTEP]
rw [← one_mul x, ← hab, add_mul]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ a * x + b * x < y
[PROOFSTEP]
exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
have hyz : y < z := by
  rw [← one_mul z, ← hab, add_mul]
  exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < z
[PROOFSTEP]
rw [← one_mul z, ← hab, add_mul]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
⊢ y < a * z + b * z
[PROOFSTEP]
exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
have : (f y - f x) * (z - y) < (f z - f y) * (y - x) :=
  (div_lt_div_iff (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
have hxz : 0 < z - x := sub_pos.2 (hxy.trans hyz)
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
have ha : (z - y) / (z - x) = a := by
  rw [eq_comm, ← sub_eq_iff_eq_add'] at hab
  simp_rw [div_eq_iff hxz.ne', ← hab]
  ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ (z - y) / (z - x) = a
[PROOFSTEP]
rw [eq_comm, ← sub_eq_iff_eq_add'] at hab
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 1 - a = b
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ (z - y) / (z - x) = a
[PROOFSTEP]
simp_rw [div_eq_iff hxz.ne', ← hab]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 1 - a = b
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
⊢ z - (a * x + (1 - a) * z) = a * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
have hb : (y - x) / (z - x) = b := by
  rw [eq_comm, ← sub_eq_iff_eq_add] at hab
  simp_rw [div_eq_iff hxz.ne', ← hab]
  ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b
[PROOFSTEP]
rw [eq_comm, ← sub_eq_iff_eq_add] at hab
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b
[PROOFSTEP]
simp_rw [div_eq_iff hxz.ne', ← hab]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (1 - b) * x + b * z - x = b * (z - x)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb✝ : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
hb : (y - x) / (z - x) = b
⊢ f (a • x + b • z) < a • f x + b • f z
[PROOFSTEP]
rwa [sub_mul, sub_mul, sub_lt_iff_lt_add', ← add_sub_assoc, lt_sub_iff_add_lt, ← mul_add, sub_add_sub_cancel, ←
  lt_div_iff hxz, add_div, mul_div_assoc, mul_div_assoc, mul_comm (f x), mul_comm (f z), ha, hb] at this
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ StrictConcaveOn 𝕜 s f
[PROOFSTEP]
rw [← neg_strictConvexOn_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ StrictConvexOn 𝕜 s (-f)
[PROOFSTEP]
refine' strictConvexOn_of_slope_strict_mono_adjacent hs fun hx hz hxy hyz => _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ ((-f) y✝ - (-f) x✝) / (y✝ - x✝) < ((-f) z✝ - (-f) y✝) / (z✝ - y✝)
[PROOFSTEP]
rw [← neg_lt_neg_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ -(((-f) z✝ - (-f) y✝) / (z✝ - y✝)) < -(((-f) y✝ - (-f) x✝) / (y✝ - x✝))
[PROOFSTEP]
simp_rw [← neg_div, neg_sub, Pi.neg_apply, neg_sub_neg]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ (f z✝ - f y✝) / (z✝ - y✝) < (f y✝ - f x✝) / (y✝ - x✝)
[PROOFSTEP]
exact hf hx hz hxy hyz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
[PROOFSTEP]
have hxy' : 0 < y - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
[PROOFSTEP]
have hyz' : 0 < z - y := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - y
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
[PROOFSTEP]
have hxz' : 0 < z - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
⊢ 0 < z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
[PROOFSTEP]
rw [← le_div_iff' hxz']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ f y ≤ ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
have ha : 0 ≤ (z - y) / (z - x) := by positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ 0 ≤ (z - y) / (z - x)
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
⊢ f y ≤ ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
have hb : 0 ≤ (y - x) / (z - x) := by positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
⊢ 0 ≤ (y - x) / (z - x)
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ f y ≤ ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
calc
  f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) := ?_
  _ ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := (hf.2 hx hz ha hb ?_)
  _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_
[GOAL]
case calc_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z)
[PROOFSTEP]
congr 1
[GOAL]
case calc_1.e_a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ y = (z - y) / (z - x) * x + (y - x) / (z - x) * z
[PROOFSTEP]
field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
[GOAL]
case calc_1.e_a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ y * (z - x) = (z - y) * x + (y - x) * z
[PROOFSTEP]
ring
[GOAL]
case calc_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ Div.div (z - y) (z - x) + Div.div (y - x) (z - x) = 1
[PROOFSTEP]
show (z - y) / (z - x) + (y - x) / (z - x) = 1
[GOAL]
case calc_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1
[PROOFSTEP]
field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
[GOAL]
case calc_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)
[PROOFSTEP]
have hxy' : 0 < y - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)
[PROOFSTEP]
have hxz' : 0 < z - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)
[PROOFSTEP]
rw [div_le_div_iff hxy' hxz']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) ≤ (f z - f x) * (y - x)
[PROOFSTEP]
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
have hyz' : 0 < z - y := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < z - y
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
have hxz' : 0 < z - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ 0 < z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
[PROOFSTEP]
rw [div_le_div_iff hxz' hyz']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) * (z - y) ≤ (f z - f y) * (z - x)
[PROOFSTEP]
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x ≤ y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
[PROOFSTEP]
rcases eq_or_lt_of_le hxy with (rfl | hxy)
[GOAL]
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x : 𝕜
ha : a ∈ s
hx : x ∈ s
hxa : x ≠ a
hy : x ∈ s
hya : x ≠ a
hxy : x ≤ x
⊢ (f x - f a) / (x - a) ≤ (f x - f a) / (x - a)
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
[PROOFSTEP]
cases' lt_or_gt_of_ne hxa with hxa hxa
[GOAL]
case inr.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
[PROOFSTEP]
cases' lt_or_gt_of_ne hya with hya hya
[GOAL]
case inr.inl.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
[PROOFSTEP]
convert hf.secant_mono_aux3 hx ha hxy hya using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
rw [← neg_div_neg_eq]
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)
[PROOFSTEP]
rw [← neg_div_neg_eq]
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
[PROOFSTEP]
field_simp
[GOAL]
case inr.inl.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y > a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
[PROOFSTEP]
convert hf.slope_mono_adjacent hx hy hxa hya using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y > a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
rw [← neg_div_neg_eq]
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y > a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
field_simp
[GOAL]
case inr.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x > a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
[PROOFSTEP]
exact hf.secant_mono_aux2 ha hy hxa hxy
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
[PROOFSTEP]
have hxy' : 0 < y - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
[PROOFSTEP]
have hyz' : 0 < z - y := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - y
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
[PROOFSTEP]
have hxz' : 0 < z - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
⊢ 0 < z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
[PROOFSTEP]
rw [← lt_div_iff' hxz']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ f y < ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
have ha : 0 < (z - y) / (z - x) := by positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ 0 < (z - y) / (z - x)
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
⊢ f y < ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
have hb : 0 < (y - x) / (z - x) := by positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
⊢ 0 < (y - x) / (z - x)
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ f y < ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
calc
  f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) := ?_
  _ < (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := (hf.2 hx hz (by linarith) ha hb ?_)
  _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ x ≠ z
[PROOFSTEP]
linarith
[GOAL]
case calc_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z)
[PROOFSTEP]
congr 1
[GOAL]
case calc_1.e_a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ y = (z - y) / (z - x) * x + (y - x) / (z - x) * z
[PROOFSTEP]
field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
[GOAL]
case calc_1.e_a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ y * (z - x) = (z - y) * x + (y - x) * z
[PROOFSTEP]
ring
[GOAL]
case calc_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ Div.div (z - y) (z - x) + Div.div (y - x) (z - x) = 1
[PROOFSTEP]
show (z - y) / (z - x) + (y - x) / (z - x) = 1
[GOAL]
case calc_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1
[PROOFSTEP]
field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
[GOAL]
case calc_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)
[PROOFSTEP]
field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
[PROOFSTEP]
have hxy' : 0 < y - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
[PROOFSTEP]
have hxz' : 0 < z - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
[PROOFSTEP]
rw [div_lt_div_iff hxy' hxz']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) < (f z - f x) * (y - x)
[PROOFSTEP]
linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)
[PROOFSTEP]
have hyz' : 0 < z - y := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < z - y
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)
[PROOFSTEP]
have hxz' : 0 < z - x := by linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
⊢ 0 < z - x
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) / (z - x) < (f z - f y) / (z - y)
[PROOFSTEP]
rw [div_lt_div_iff hxz' hyz']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) * (z - y) < (f z - f y) * (z - x)
[PROOFSTEP]
linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
[PROOFSTEP]
cases' lt_or_gt_of_ne hxa with hxa hxa
[GOAL]
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : x < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
[PROOFSTEP]
cases' lt_or_gt_of_ne hya with hya hya
[GOAL]
case inl.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
[PROOFSTEP]
convert hf.secant_strict_mono_aux3 hx ha hxy hya using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
rw [← neg_div_neg_eq]
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)
[PROOFSTEP]
rw [← neg_div_neg_eq]
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
[PROOFSTEP]
field_simp
[GOAL]
case inl.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y > a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
[PROOFSTEP]
convert hf.slope_strict_mono_adjacent hx hy hxa hya using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y > a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
rw [← neg_div_neg_eq]
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y > a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
[PROOFSTEP]
field_simp
[GOAL]
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy : x < y
hxa : x > a
⊢ (f x - f a) / (x - a) < (f y - f a) / (y - a)
[PROOFSTEP]
exact hf.secant_strict_mono_aux2 ha hy hxa hxy
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
[PROOFSTEP]
have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
[PROOFSTEP]
simp only [Pi.neg_apply] at key
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
[PROOFSTEP]
rw [← neg_lt_neg_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ -((f x - f a) / (x - a)) < -((f y - f a) / (y - a))
[PROOFSTEP]
convert key using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ -((f x - f a) / (x - a)) = (-f x - -f a) / (x - a)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ -((f y - f a) / (y - a)) = (-f y - -f a) / (y - a)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f a - f x) / (x - a) = (-f x + f a) / (x - a)
[PROOFSTEP]
ring
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f a - f y) / (y - a) = (-f y + f a) / (y - a)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Ici y)
[PROOFSTEP]
intro u hu v hv huv
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
⊢ f u < f v
[PROOFSTEP]
have step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z :=
  by
  intros z hz
  refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
  rw [openSegment_eq_Ioo (hxy.trans hz.2)]
  exact ⟨hxy, hz.2⟩
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
⊢ ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
[PROOFSTEP]
intros z hz
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ f y < f z
[PROOFSTEP]
refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ openSegment 𝕜 x z
[PROOFSTEP]
rw [openSegment_eq_Ioo (hxy.trans hz.2)]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
z : 𝕜
hz : z ∈ s ∩ Set.Ioi y
⊢ y ∈ Set.Ioo x z
[PROOFSTEP]
exact ⟨hxy, hz.2⟩
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
⊢ f u < f v
[PROOFSTEP]
rcases eq_or_lt_of_le hu.2 with (rfl | hu2)
[GOAL]
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu : y ∈ s ∩ Set.Ici y
huv : y < v
⊢ f y < f v
[PROOFSTEP]
exact step1 ⟨hv.1, huv⟩
[GOAL]
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ f u < f v
[PROOFSTEP]
refine' hf.lt_right_of_left_lt _ hv.1 _ (step1 ⟨hu.1, hu2⟩)
[GOAL]
case inr.refine'_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ s
[PROOFSTEP]
apply hf.1.segment_subset hx hu.1
[GOAL]
case inr.refine'_1.a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ segment 𝕜 x u
[PROOFSTEP]
rw [segment_eq_Icc (hxy.le.trans hu.2)]
[GOAL]
case inr.refine'_1.a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ Set.Icc x u
[PROOFSTEP]
exact ⟨hxy.le, hu.2⟩
[GOAL]
case inr.refine'_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ openSegment 𝕜 y v
[PROOFSTEP]
rw [openSegment_eq_Ioo (hu2.trans huv)]
[GOAL]
case inr.refine'_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ Set.Ioo y v
[PROOFSTEP]
exact ⟨hu2, huv⟩


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
c : ℝ
hc : 0 < c
y : H
hy : y ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ inner x (c • y)
[PROOFSTEP]
rw [real_inner_smul_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
c : ℝ
hc : 0 < c
y : H
hy : y ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ c * inner x y
[PROOFSTEP]
exact mul_nonneg hc.le (hy x hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
u : H
hu : u ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
v : H
hv : v ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ inner x (u + v)
[PROOFSTEP]
rw [inner_add_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t s : Set H
u : H
hu : u ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
v : H
hv : v ∈ {y | ∀ (x : H), x ∈ s → 0 ≤ inner x y}
x : H
hx : x ∈ s
⊢ 0 ≤ inner x u + inner x v
[PROOFSTEP]
exact add_nonneg (hu x hx) (hv x hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ innerDualCone univ = 0
[PROOFSTEP]
suffices ∀ x : H, x ∈ (univ : Set H).innerDualCone → x = 0
  by
  apply SetLike.coe_injective
  exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ innerDualCone univ = 0
[PROOFSTEP]
apply SetLike.coe_injective
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
this : ∀ (x : H), x ∈ innerDualCone univ → x = 0
⊢ ↑(innerDualCone univ) = ↑0
[PROOFSTEP]
exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (x : H), x ∈ innerDualCone univ → x = 0
[PROOFSTEP]
exact fun x hx => by simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : H
hx : x ∈ innerDualCone univ
⊢ x = 0
[PROOFSTEP]
simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : H
x✝ : x ∈ s
⊢ 0 ≤ inner x 0
[PROOFSTEP]
rw [inner_zero_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s✝ t : Set H
x : H
s : Set H
⊢ innerDualCone (insert x s) = innerDualCone {x} ⊓ innerDualCone s
[PROOFSTEP]
rw [insert_eq, innerDualCone_union]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
⊢ innerDualCone (⋃ (i : ι), f i) = ⨅ (i : ι), innerDualCone (f i)
[PROOFSTEP]
refine' le_antisymm (le_iInf fun i x hx y hy => hx _ <| mem_iUnion_of_mem _ hy) _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
⊢ ⨅ (i : ι), innerDualCone (f i) ≤ innerDualCone (⋃ (i : ι), f i)
[PROOFSTEP]
intro x hx y hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
x : H
hx : x ∈ ⨅ (i : ι), innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
[PROOFSTEP]
rw [ConvexCone.mem_iInf] at hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
⊢ 0 ≤ inner y x
[PROOFSTEP]
obtain ⟨j, hj⟩ := mem_iUnion.mp hy
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
ι : Sort u_6
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ innerDualCone (f i)
y : H
hy : y ∈ ⋃ (i : ι), f i
j : ι
hj : y ∈ f j
⊢ 0 ≤ inner y x
[PROOFSTEP]
exact hx _ _ hj
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
S : Set (Set H)
⊢ innerDualCone (⋃₀ S) = sInf (innerDualCone '' S)
[PROOFSTEP]
simp_rw [sInf_image, sUnion_eq_biUnion, innerDualCone_iUnion]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ↑(innerDualCone s) = ⋂ (i : ↑s), ↑(innerDualCone {↑i})
[PROOFSTEP]
rw [← ConvexCone.coe_iInf, ← innerDualCone_iUnion, iUnion_of_singleton_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed ↑(innerDualCone s)
[PROOFSTEP]
rw [innerDualCone_eq_iInter_innerDualCone_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ IsClosed (⋂ (i : ↑s), ↑(innerDualCone {↑i}))
[PROOFSTEP]
apply isClosed_iInter
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ∀ (i : ↑s), IsClosed ↑(innerDualCone {↑i})
[PROOFSTEP]
intro x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ IsClosed ↑(innerDualCone {↑x})
[PROOFSTEP]
have h : ({↑x} : Set H).innerDualCone = (inner x : H → ℝ) ⁻¹' Set.Ici 0 := by
  rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]
    -- the preimage is closed as `inner x` is continuous and `[0, ∞)` is closed
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
⊢ ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
[PROOFSTEP]
rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]
  -- the preimage is closed as `inner x` is continuous and `[0, ∞)` is closed
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed ↑(innerDualCone {↑x})
[PROOFSTEP]
rw [h]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
x : ↑s
h : ↑(innerDualCone {↑x}) = inner ↑x ⁻¹' Ici 0
⊢ IsClosed (inner ↑x ⁻¹' Ici 0)
[PROOFSTEP]
exact isClosed_Ici.preimage (continuous_const.inner continuous_id')
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
⊢ Pointed K
[PROOFSTEP]
obtain ⟨x, hx⟩ := ne
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
⊢ Pointed K
[PROOFSTEP]
let f : ℝ → H :=
  (· • x)
    -- f (0, ∞) is a subset of K
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ Pointed K
[PROOFSTEP]
have fI : f '' Set.Ioi 0 ⊆ (K : Set H) := by
  rintro _ ⟨_, h, rfl⟩
  exact K.smul_mem (Set.mem_Ioi.1 h) hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ f '' Ioi 0 ⊆ ↑K
[PROOFSTEP]
rintro _ ⟨_, h, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
w✝ : ℝ
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑K
[PROOFSTEP]
exact K.smul_mem (Set.mem_Ioi.1 h) hx
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
⊢ Pointed K
[PROOFSTEP]
have clf : closure (f '' Set.Ioi 0) ⊆ (K : Set H) := hc.closure_subset_iff.2 fI
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
⊢ Pointed K
[PROOFSTEP]
have fc : ContinuousWithinAt f (Set.Ioi (0 : ℝ)) 0 := (continuous_id.smul continuous_const).continuousWithinAt
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ Pointed K
[PROOFSTEP]
have mem₀ :=
  fc.mem_closure_image
    (by rw [closure_Ioi (0 : ℝ), mem_Ici])
      -- as 0 ∈ closure f (0, ∞) and closure f (0, ∞) ⊆ K, 0 ∈ K.
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)
[PROOFSTEP]
rw [closure_Ioi (0 : ℝ), mem_Ici]
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
⊢ Pointed K
[PROOFSTEP]
have f₀ : f 0 = 0 := zero_smul ℝ x
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
f₀ : f 0 = 0
⊢ Pointed K
[PROOFSTEP]
simpa only [f₀, ConvexCone.Pointed, ← SetLike.mem_coe] using mem_of_subset_of_mem clf mem₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
⊢ ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner y b < 0
[PROOFSTEP]
obtain ⟨z, hzK, infi⟩ := exists_norm_eq_iInf_of_complete_convex ne hc.isComplete K.convex b
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
⊢ ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner y b < 0
[PROOFSTEP]
have hinner := (norm_eq_iInf_iff_real_inner_le_zero K.convex hzK).1 infi
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ ∃ y, (∀ (x : H), x ∈ K → 0 ≤ inner x y) ∧ inner y b < 0
[PROOFSTEP]
use z - b
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ (∀ (x : H), x ∈ K → 0 ≤ inner x (z - b)) ∧ inner (z - b) b < 0
[PROOFSTEP]
constructor
[GOAL]
case h.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ ∀ (x : H), x ∈ K → 0 ≤ inner x (z - b)
[PROOFSTEP]
rintro x hxK
[GOAL]
case h.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
x : H
hxK : x ∈ K
⊢ 0 ≤ inner x (z - b)
[PROOFSTEP]
specialize hinner _ (K.add_mem hxK hzK)
[GOAL]
case h.left
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
x : H
hxK : x ∈ K
hinner : inner (b - z) (x + z - z) ≤ 0
⊢ 0 ≤ inner x (z - b)
[PROOFSTEP]
rwa [add_sub_cancel, real_inner_comm, ← neg_nonneg, neg_eq_neg_one_mul, ← real_inner_smul_right, neg_smul, one_smul,
  neg_sub] at hinner
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
⊢ inner (z - b) b < 0
[PROOFSTEP]
have hinner₀ :=
  hinner 0
    (K.pointed_of_nonempty_of_isClosed ne hc)
      -- the rest of the proof is a straightforward calculation
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : inner (b - z) (0 - z) ≤ 0
⊢ inner (z - b) b < 0
[PROOFSTEP]
rw [zero_sub, inner_neg_right, Right.neg_nonpos_iff] at hinner₀
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
⊢ inner (z - b) b < 0
[PROOFSTEP]
have hbz : b - z ≠ 0 := by
  rw [sub_ne_zero]
  contrapose! hzK
  rwa [← hzK]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
⊢ b - z ≠ 0
[PROOFSTEP]
rw [sub_ne_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
⊢ b ≠ z
[PROOFSTEP]
contrapose! hzK
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hzK : b = z
⊢ ¬z ∈ ↑K
[PROOFSTEP]
rwa [← hzK]
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hbz : b - z ≠ 0
⊢ inner (z - b) b < 0
[PROOFSTEP]
rw [← neg_zero, lt_neg, ← neg_one_mul, ← real_inner_smul_left, smul_sub, neg_smul, one_smul, neg_smul, neg_sub_neg,
  one_smul]
[GOAL]
case h.right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hbz : b - z ≠ 0
⊢ 0 < inner (b - z) b
[PROOFSTEP]
calc
  0 < ⟪b - z, b - z⟫_ℝ := lt_of_not_le ((Iff.not real_inner_self_nonpos).2 hbz)
  _ = ⟪b - z, b - z⟫_ℝ + 0 := (add_zero _).symm
  _ ≤ ⟪b - z, b - z⟫_ℝ + ⟪b - z, z⟫_ℝ := (add_le_add rfl.ge hinner₀)
  _ = ⟪b - z, b - z + z⟫_ℝ := (inner_add_right _ _ _).symm
  _ = ⟪b - z, b⟫_ℝ := by rw [sub_add_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
b : H
disj : ¬b ∈ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ (w : ↑↑K), ‖b - ↑w‖
hinner : ∀ (w : H), w ∈ ↑K → inner (b - z) (w - z) ≤ 0
hinner₀ : 0 ≤ inner (b - z) z
hbz : b - z ≠ 0
⊢ inner (b - z) (b - z + z) = inner (b - z) b
[PROOFSTEP]
rw [sub_add_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
⊢ innerDualCone ↑(innerDualCone ↑K) = K
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) ↔ x ∈ K
[PROOFSTEP]
constructor
[GOAL]
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ innerDualCone ↑(innerDualCone ↑K) → x ∈ K
[PROOFSTEP]
rw [mem_innerDualCone, ← SetLike.mem_coe]
[GOAL]
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ (∀ (x_1 : H), x_1 ∈ ↑(innerDualCone ↑K) → 0 ≤ inner x_1 x) → x ∈ ↑K
[PROOFSTEP]
contrapose!
[GOAL]
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ ¬x ∈ ↑K → ∃ x_1, x_1 ∈ ↑(innerDualCone ↑K) ∧ inner x_1 x < 0
[PROOFSTEP]
exact K.hyperplane_separation_of_nonempty_of_isClosed_of_nmem ne hc
[GOAL]
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
⊢ x ∈ K → x ∈ innerDualCone ↑(innerDualCone ↑K)
[PROOFSTEP]
rintro hxK y h
[GOAL]
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : y ∈ ↑(innerDualCone ↑K)
⊢ 0 ≤ inner y x
[PROOFSTEP]
specialize h x hxK
[GOAL]
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
s t : Set H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : 0 ≤ inner x y
⊢ 0 ≤ inner y x
[PROOFSTEP]
rwa [real_inner_comm]


[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_monomial n c =>
  simpa [exp_neg, div_eq_mul_inv, mul_assoc] using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
| h_add p q hp hq => simpa [add_div] using hp.add hq
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_monomial n c =>
  simpa [exp_neg, div_eq_mul_inv, mul_assoc] using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
| h_add p q hp hq => simpa [add_div] using hp.add hq
[GOAL]
case h_monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x => eval x (↑(monomial n) c) / exp x) atTop (𝓝 0)
[PROOFSTEP]

| h_monomial n c =>
  simpa [exp_neg, div_eq_mul_inv, mul_assoc] using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
[GOAL]
case h_monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x => eval x (↑(monomial n) c) / exp x) atTop (𝓝 0)
[PROOFSTEP]
simpa [exp_neg, div_eq_mul_inv, mul_assoc] using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
[GOAL]
case h_add
p q : ℝ[X]
hp : Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
hq : Tendsto (fun x => eval x q / exp x) atTop (𝓝 0)
⊢ Tendsto (fun x => eval x (p + q) / exp x) atTop (𝓝 0)
[PROOFSTEP]

| h_add p q hp hq => simpa [add_div] using hp.add hq
[GOAL]
case h_add
p q : ℝ[X]
hp : Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
hq : Tendsto (fun x => eval x q / exp x) atTop (𝓝 0)
⊢ Tendsto (fun x => eval x (p + q) / exp x) atTop (𝓝 0)
[PROOFSTEP]
simpa [add_div] using hp.add hq