⊢ ∀ {x y z : ℝ}, x ∈ Ioi 0 → z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
⊢ StrictConcaveOn ℝ (Ioi 0) log
apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
⊢ ∀ {x y z : ℝ}, x ∈ Ioi 0 → z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
rintro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
have hy : 0 < y := hx.trans hxy
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < y⁻¹

x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ y⁻¹ < (log y - log x) / (y - x)
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
trans y⁻¹
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ (log z - log y) / (z - y) < y⁻¹
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (log z - log y) / (z - y) < y⁻¹
have h : 0 < z - y := by linarith
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ log z - log y < y⁻¹ * (z - y)
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ (log z - log y) / (z - y) < y⁻¹
rw [div_lt_iff h]
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
⊢ log z - log y < y⁻¹ * (z - y)
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ log z - log y < y⁻¹ * (z - y)
have hyz' : 0 < z / y := by positivity
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y < y⁻¹ * (z - y)
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
⊢ log z - log y < y⁻¹ * (z - y)
have hyz'' : z / y ≠ 1 := by
  contrapose! h
  rw [div_eq_one_iff_eq hy.ne'] at h
  simp [h]
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y < y⁻¹ * (z - y)
calc
  log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
  _ < z / y - 1 := (log_lt_sub_one_of_pos hyz' hyz'')
  _ = y⁻¹ * (z - y) := by field_simp [hy.ne']
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < z - y
linarith
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
⊢ 0 < z / y
positivity
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hyz' : 0 < z / y
h : z / y = 1
⊢ z - y ≤ 0
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
⊢ z / y ≠ 1
contrapose! h
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hyz' : 0 < z / y
h : z = y
⊢ z - y ≤ 0
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hyz' : 0 < z / y
h : z / y = 1
⊢ z - y ≤ 0
rw [div_eq_one_iff_eq hy.ne'] at h
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hyz' : 0 < z / y
h : z = y
⊢ z - y ≤ 0
simp [h]
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y = log (z / y)
rw [← log_div hz.ne' hy.ne']
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ z / y - 1 = y⁻¹ * (z - y)
field_simp [hy.ne']
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ y⁻¹ < (log y - log x) / (y - x)
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ y⁻¹ < (log y - log x) / (y - x)
have h : 0 < y - x := by linarith
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ y⁻¹ * (y - x) < log y - log x
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ y⁻¹ < (log y - log x) / (y - x)
rw [lt_div_iff h]
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
⊢ y⁻¹ * (y - x) < log y - log x
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ y⁻¹ * (y - x) < log y - log x
have hxy' : 0 < x / y := by positivity
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ y⁻¹ * (y - x) < log y - log x
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
⊢ y⁻¹ * (y - x) < log y - log x
have hxy'' : x / y ≠ 1 := by
  contrapose! h
  rw [div_eq_one_iff_eq hy.ne'] at h
  simp [h]
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ y⁻¹ * (y - x) < log y - log x
calc
  y⁻¹ * (y - x) = 1 - x / y := by field_simp [hy.ne']
  _ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy'']
  _ = -(log x - log y) := by rw [log_div hx.ne' hy.ne']
  _ = log y - log x := by ring
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < y - x
linarith
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ 0 < x / y
positivity
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hxy' : 0 < x / y
h : x / y = 1
⊢ y - x ≤ 0
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
⊢ x / y ≠ 1
contrapose! h
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hxy' : 0 < x / y
h : x = y
⊢ y - x ≤ 0
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hxy' : 0 < x / y
h : x / y = 1
⊢ y - x ≤ 0
rw [div_eq_one_iff_eq hy.ne'] at h
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
hxy' : 0 < x / y
h : x = y
⊢ y - x ≤ 0
simp [h]
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ y⁻¹ * (y - x) = 1 - x / y
field_simp [hy.ne']
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ 1 - x / y < -log (x / y)
linarith [log_lt_sub_one_of_pos hxy' hxy'']
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ -log (x / y) = -(log x - log y)
rw [log_div hx.ne' hy.ne']
no goals
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ -(log x - log y) = log y - log x
ring