[GOAL]
⊢ StrictConvexOn ℝ univ exp
[PROOFSTEP]
apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ
[GOAL]
⊢ ∀ {x y z : ℝ}, x ∈ univ → z ∈ univ → x < y → y < z → (exp y - exp x) / (y - x) < (exp z - exp y) / (z - y)
[PROOFSTEP]
rintro x y z - - hxy hyz
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (exp y - exp x) / (y - x) < (exp z - exp y) / (z - y)
[PROOFSTEP]
trans exp y
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ (exp y - exp x) / (y - x) < exp y
[PROOFSTEP]
have h1 : 0 < y - x := by linarith
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < y - x
[PROOFSTEP]
linarith
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (exp y - exp x) / (y - x) < exp y
[PROOFSTEP]
have h2 : x - y < 0 := by linarith
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ x - y < 0
[PROOFSTEP]
linarith
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (exp y - exp x) / (y - x) < exp y
[PROOFSTEP]
rw [div_lt_iff h1]
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x < exp y * (y - x)
[PROOFSTEP]
calc
  exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
  _ = exp y * (1 - exp (x - y)) := by ring
  _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp_of_nonzero h2.ne]
  _ = exp y * (y - x) := by ring
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x = exp y - exp y * exp (x - y)
[PROOFSTEP]
rw [← exp_add]
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp x = exp y - exp (y + (x - y))
[PROOFSTEP]
ring_nf
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y - exp y * exp (x - y) = exp y * (1 - exp (x - y))
[PROOFSTEP]
ring
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y * (1 - exp (x - y)) < exp y * -(x - y)
[PROOFSTEP]
gcongr
[GOAL]
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ 1 - exp (x - y) < -(x - y)
[PROOFSTEP]
linarith [add_one_lt_exp_of_nonzero h2.ne]
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ exp y * -(x - y) = exp y * (y - x)
[PROOFSTEP]
ring
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ exp y < (exp z - exp y) / (z - y)
[PROOFSTEP]
have h1 : 0 < z - y := by linarith
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
⊢ 0 < z - y
[PROOFSTEP]
linarith
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y < (exp z - exp y) / (z - y)
[PROOFSTEP]
rw [lt_div_iff h1]
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (z - y) < exp z - exp y
[PROOFSTEP]
calc
  exp y * (z - y) < exp y * (exp (z - y) - 1) := by
    gcongr _ * ?_
    linarith [add_one_lt_exp_of_nonzero h1.ne']
  _ = exp (z - y) * exp y - exp y := by ring
  _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (z - y) < exp y * (exp (z - y) - 1)
[PROOFSTEP]
gcongr _ * ?_
[GOAL]
case bc
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ z - y < exp (z - y) - 1
[PROOFSTEP]
linarith [add_one_lt_exp_of_nonzero h1.ne']
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp y * (exp (z - y) - 1) = exp (z - y) * exp y - exp y
[PROOFSTEP]
ring
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp (z - y) * exp y - exp y ≤ exp z - exp y
[PROOFSTEP]
rw [← exp_add]
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp (z - y + y) - exp y ≤ exp z - exp y
[PROOFSTEP]
ring_nf
[GOAL]
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < z - y
⊢ exp z - exp y ≤ exp z - exp y
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ n
[PROOFSTEP]
induction' n with k IH
[GOAL]
case zero
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ Nat.zero
[PROOFSTEP]
exact convexOn_const (1 : ℝ) (convex_Ici _)
[GOAL]
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ Nat.succ k
[PROOFSTEP]
refine' ⟨convex_Ici _, _⟩
[GOAL]
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ici 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ici 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun x => x ^ Nat.succ k) (a • x + b • y) ≤
                    a • (fun x => x ^ Nat.succ k) x + b • (fun x => x ^ Nat.succ k) y
[PROOFSTEP]
rintro a (ha : 0 ≤ a) b (hb : 0 ≤ b) μ ν hμ hν h
[GOAL]
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
[PROOFSTEP]
have H := IH.2 ha hb hμ hν h
[GOAL]
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
[PROOFSTEP]
have : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν :=
  by
  cases' le_or_lt a b with hab hab
  · have : a ^ k ≤ b ^ k := by gcongr
    have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
    positivity
  · have : b ^ k ≤ a ^ k := by gcongr
    have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
    positivity
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
have : a ^ k ≤ b ^ k := by gcongr
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
⊢ a ^ k ≤ b ^ k
[PROOFSTEP]
gcongr
[GOAL]
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this : a ^ k ≤ b ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this : a ^ k ≤ b ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a)
[PROOFSTEP]
nlinarith
[GOAL]
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this✝ : a ^ k ≤ b ^ k
this : 0 ≤ (b ^ k - a ^ k) * (b - a)
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
positivity
[GOAL]
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
have : b ^ k ≤ a ^ k := by gcongr
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
⊢ b ^ k ≤ a ^ k
[PROOFSTEP]
gcongr
[GOAL]
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this : b ^ k ≤ a ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this : b ^ k ≤ a ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a)
[PROOFSTEP]
nlinarith
[GOAL]
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this✝ : b ^ k ≤ a ^ k
this : 0 ≤ (b ^ k - a ^ k) * (b - a)
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
positivity
[GOAL]
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
[PROOFSTEP]
calc
  (μ * a + ν * b) ^ k.succ = (μ * a + ν * b) * (μ * a + ν * b) ^ k := pow_succ _ _
  _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) := by gcongr; exact H
  _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν := by linarith
  _ = (μ + ν) * (μ * a ^ k.succ + ν * b ^ k.succ) := by rw [Nat.succ_eq_add_one]; ring
  _ = μ * a ^ k.succ + ν * b ^ k.succ := by rw [h]; ring
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a + ν * b) ^ k ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k)
[PROOFSTEP]
gcongr
[GOAL]
case h
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) ^ k ≤ μ * a ^ k + ν * b ^ k
[PROOFSTEP]
exact H
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) ≤
    (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν =
    (μ + ν) * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν =
    (μ + ν) * (μ * a ^ (k + 1) + ν * b ^ (k + 1))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ + ν) * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k) = μ * a ^ Nat.succ k + ν * b ^ Nat.succ k
[PROOFSTEP]
rw [h]
[GOAL]
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ 1 * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k) = μ * a ^ Nat.succ k + ν * b ^ Nat.succ k
[PROOFSTEP]
ring
[GOAL]
n : ℕ
hn : Even n
⊢ ConvexOn ℝ univ fun x => x ^ n
[PROOFSTEP]
refine' ⟨convex_univ, _⟩
[GOAL]
n : ℕ
hn : Even n
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ univ →
      ∀ ⦃y : ℝ⦄,
        y ∈ univ →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → (fun x => x ^ n) (a • x + b • y) ≤ a • (fun x => x ^ n) x + b • (fun x => x ^ n) y
[PROOFSTEP]
rintro a - b - μ ν hμ hν h
[GOAL]
n : ℕ
hn : Even n
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => x ^ n) (μ • a + ν • b) ≤ μ • (fun x => x ^ n) a + ν • (fun x => x ^ n) b
[PROOFSTEP]
obtain ⟨k, rfl⟩ :=
  hn.exists_two_nsmul
    _
      -- Porting note: added type ascription to LHS
[GOAL]
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
⊢ (fun x => x ^ (2 • k)) (μ • a + ν • b) ≤ μ • (fun x => x ^ (2 • k)) a + ν • (fun x => x ^ (2 • k)) b
[PROOFSTEP]
have : (0 : ℝ) ≤ (a - b) ^ 2 * μ * ν := by positivity
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
⊢ 0 ≤ (a - b) ^ 2 * μ * ν
[PROOFSTEP]
positivity
[GOAL]
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (fun x => x ^ (2 • k)) (μ • a + ν • b) ≤ μ • (fun x => x ^ (2 • k)) a + ν • (fun x => x ^ (2 • k)) b
[PROOFSTEP]
calc
  (μ * a + ν * b) ^ (2 * k) = ((μ * a + ν * b) ^ 2) ^ k := by rw [pow_mul]
  _ ≤ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k := by gcongr; linarith
  _ = (μ * a ^ 2 + ν * b ^ 2) ^ k := by rw [h]; ring
  _ ≤ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k := ?_
  _ ≤ μ * a ^ (2 * k) + ν * b ^ (2 * k) := by ring_nf;
    rfl
      -- Porting note: `rw [mem_Ici]` was `dsimp`
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a + ν * b) ^ (2 * k) = ((μ * a + ν * b) ^ 2) ^ k
[PROOFSTEP]
rw [pow_mul]
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ ((μ * a + ν * b) ^ 2) ^ k ≤ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k
[PROOFSTEP]
gcongr
[GOAL]
case hab
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a + ν * b) ^ 2 ≤ (μ + ν) * (μ * a ^ 2 + ν * b ^ 2)
[PROOFSTEP]
linarith
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k = (μ * a ^ 2 + ν * b ^ 2) ^ k
[PROOFSTEP]
rw [h]
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (1 * (μ * a ^ 2 + ν * b ^ 2)) ^ k = (μ * a ^ 2 + ν * b ^ 2) ^ k
[PROOFSTEP]
ring
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k ≤ μ * a ^ (2 * k) + ν * b ^ (2 * k)
[PROOFSTEP]
ring_nf
[GOAL]
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ μ * a ^ (k * 2) + ν * b ^ (k * 2) ≤ μ * a ^ (k * 2) + ν * b ^ (k * 2)
[PROOFSTEP]
rfl
  -- Porting note: `rw [mem_Ici]` was `dsimp`
[GOAL]
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a ^ 2 + ν * b ^ 2) ^ k ≤ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k
[PROOFSTEP]
refine' (convexOn_pow k).2 _ _ hμ hν h
[GOAL]
case intro.refine'_1
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ a ^ 2 ∈ Ici 0
[PROOFSTEP]
rw [mem_Ici]
[GOAL]
case intro.refine'_2
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ b ^ 2 ∈ Ici 0
[PROOFSTEP]
rw [mem_Ici]
[GOAL]
case intro.refine'_1
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ 0 ≤ a ^ 2
[PROOFSTEP]
positivity
[GOAL]
case intro.refine'_2
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ 0 ≤ b ^ 2
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ ↑n
[PROOFSTEP]
simp_rw [zpow_ofNat]
[GOAL]
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ n
[PROOFSTEP]
exact (convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)
[GOAL]
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ -[n+1]
[PROOFSTEP]
simp_rw [zpow_negSucc]
[GOAL]
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => (x ^ (n + 1))⁻¹
[PROOFSTEP]
refine' ⟨convex_Ioi _, _⟩
[GOAL]
n : ℕ
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ioi 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ioi 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun x => (x ^ (n + 1))⁻¹) (a • x + b • y) ≤
                    a • (fun x => (x ^ (n + 1))⁻¹) x + b • (fun x => (x ^ (n + 1))⁻¹) y
[PROOFSTEP]
rintro a (ha : 0 < a) b (hb : 0 < b) μ ν hμ hν h
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => (x ^ (n + 1))⁻¹) (μ • a + ν • b) ≤ μ • (fun x => (x ^ (n + 1))⁻¹) a + ν • (fun x => (x ^ (n + 1))⁻¹) b
[PROOFSTEP]
field_simp [ha.ne', hb.ne']
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 / (μ * a + ν * b) ^ (n + 1) ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) / (a ^ (n + 1) * b ^ (n + 1))
[PROOFSTEP]
rw [div_le_div_iff]
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1)
[PROOFSTEP]
calc
  (1 : ℝ) * (a ^ (n + 1) * b ^ (n + 1)) = ((μ + ν) ^ 2 * (a * b)) ^ (n + 1) := by rw [h]; ring
  _ ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1) := ?_
  _ = (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1) := by rw [mul_pow]
  _ ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1) := ?_
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) = ((μ + ν) ^ 2 * (a * b)) ^ (n + 1)
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) = (1 ^ 2 * (a * b)) ^ (n + 1)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1) = (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1)
[PROOFSTEP]
rw [mul_pow]
[GOAL]
case calc_1
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ ((μ + ν) ^ 2 * (a * b)) ^ (n + 1) ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1)
[PROOFSTEP]
gcongr(?_ : ℝ) ^ _
[GOAL]
case calc_1.hab
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ + ν) ^ 2 * (a * b) ≤ (μ * b + ν * a) * (μ * a + ν * b)
[PROOFSTEP]
have : (0 : ℝ) ≤ μ * ν * (a - b) ^ 2 := by positivity
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 ≤ μ * ν * (a - b) ^ 2
[PROOFSTEP]
positivity
[GOAL]
case calc_1.hab
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
this : 0 ≤ μ * ν * (a - b) ^ 2
⊢ (μ + ν) ^ 2 * (a * b) ≤ (μ * b + ν * a) * (μ * a + ν * b)
[PROOFSTEP]
linarith
[GOAL]
case calc_2
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1) ≤
    (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1)
[PROOFSTEP]
gcongr
[GOAL]
case calc_2.h
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ * b + ν * a) ^ (n + 1) ≤ μ * b ^ (n + 1) + ν * a ^ (n + 1)
[PROOFSTEP]
apply (convexOn_pow (n + 1)).2 hb.le ha.le hμ hν h
[GOAL]
case b0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < (μ * a + ν * b) ^ (n + 1)
[PROOFSTEP]
have : 0 < μ * a + ν * b := by cases le_or_lt a b <;> nlinarith
[GOAL]
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < μ * a + ν * b
[PROOFSTEP]
cases le_or_lt a b
[GOAL]
case inl
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
h✝ : a ≤ b
⊢ 0 < μ * a + ν * b
[PROOFSTEP]
nlinarith
[GOAL]
case inr
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
h✝ : b < a
⊢ 0 < μ * a + ν * b
[PROOFSTEP]
nlinarith
[GOAL]
case b0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
this : 0 < μ * a + ν * b
⊢ 0 < (μ * a + ν * b) ^ (n + 1)
[PROOFSTEP]
positivity
[GOAL]
case d0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < a ^ (n + 1) * b ^ (n + 1)
[PROOFSTEP]
positivity
[GOAL]
⊢ StrictConcaveOn ℝ (Ioi 0) log
[PROOFSTEP]
apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
[GOAL]
⊢ ∀ {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)
[PROOFSTEP]
rintro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz
[GOAL]
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)
[PROOFSTEP]
have hy : 0 < y := hx.trans hxy
[GOAL]
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)
[PROOFSTEP]
trans y⁻¹
[GOAL]
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⁻¹
[PROOFSTEP]
have h : 0 < z - y := by linarith
[GOAL]
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < z - y
[PROOFSTEP]
linarith
[GOAL]
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⁻¹
[PROOFSTEP]
rw [div_lt_iff h]
[GOAL]
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)
[PROOFSTEP]
have hyz' : 0 < z / y := by positivity
[GOAL]
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
[PROOFSTEP]
positivity
[GOAL]
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)
[PROOFSTEP]
have hyz'' : z / y ≠ 1 := by
  contrapose! h
  rw [div_eq_one_iff_eq hy.ne'] at h 
  simp [h]
[GOAL]
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
[PROOFSTEP]
contrapose! h
[GOAL]
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
[PROOFSTEP]
rw [div_eq_one_iff_eq hy.ne'] at h 
[GOAL]
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
[PROOFSTEP]
simp [h]
[GOAL]
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)
[PROOFSTEP]
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']
[GOAL]
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)
[PROOFSTEP]
rw [← log_div hz.ne' hy.ne']
[GOAL]
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)
[PROOFSTEP]
field_simp [hy.ne']
[GOAL]
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)
[PROOFSTEP]
have h : 0 < y - x := by linarith
[GOAL]
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ 0 < y - x
[PROOFSTEP]
linarith
[GOAL]
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)
[PROOFSTEP]
rw [lt_div_iff h]
[GOAL]
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
[PROOFSTEP]
have hxy' : 0 < x / y := by positivity
[GOAL]
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
[PROOFSTEP]
positivity
[GOAL]
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
[PROOFSTEP]
have hxy'' : x / y ≠ 1 := by
  contrapose! h
  rw [div_eq_one_iff_eq hy.ne'] at h 
  simp [h]
[GOAL]
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
[PROOFSTEP]
contrapose! h
[GOAL]
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
[PROOFSTEP]
rw [div_eq_one_iff_eq hy.ne'] at h 
[GOAL]
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
[PROOFSTEP]
simp [h]
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
field_simp [hy.ne']
[GOAL]
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)
[PROOFSTEP]
linarith [log_lt_sub_one_of_pos hxy' hxy'']
[GOAL]
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)
[PROOFSTEP]
rw [log_div hx.ne' hy.ne']
[GOAL]
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
[PROOFSTEP]
ring
[GOAL]
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
⊢ 1 + p * s < (1 + s) ^ p
[PROOFSTEP]
rcases eq_or_lt_of_le hs with (rfl | hs)
[GOAL]
case inl
p : ℝ
hp : 1 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 + p * -1 < (1 + -1) ^ p
[PROOFSTEP]
have : p ≠ 0 := by positivity
[GOAL]
p : ℝ
hp : 1 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ p ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case inl
p : ℝ
hp : 1 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
this : p ≠ 0
⊢ 1 + p * -1 < (1 + -1) ^ p
[PROOFSTEP]
simpa [zero_rpow this]
[GOAL]
case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
⊢ 1 + p * s < (1 + s) ^ p
[PROOFSTEP]
have hs1 : 0 < 1 + s := by linarith
[GOAL]
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
⊢ 0 < 1 + s
[PROOFSTEP]
linarith
[GOAL]
case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
⊢ 1 + p * s < (1 + s) ^ p
[PROOFSTEP]
cases' le_or_lt (1 + p * s) 0 with hs2 hs2
[GOAL]
case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 1 + p * s ≤ 0
⊢ 1 + p * s < (1 + s) ^ p
[PROOFSTEP]
exact hs2.trans_lt (rpow_pos_of_pos hs1 _)
[GOAL]
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ 1 + p * s < (1 + s) ^ p
[PROOFSTEP]
rw [rpow_def_of_pos hs1, ← exp_log hs2]
[GOAL]
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ exp (log (1 + p * s)) < exp (log (1 + s) * p)
[PROOFSTEP]
apply exp_strictMono
[GOAL]
case inr.inr.a
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ log (1 + p * s) < log (1 + s) * p
[PROOFSTEP]
have hp : 0 < p := by positivity
[GOAL]
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
case inr.inr.a
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
⊢ log (1 + p * s) < log (1 + s) * p
[PROOFSTEP]
have hs3 : 1 + s ≠ 1 := by contrapose! hs'; linarith
[GOAL]
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
⊢ 1 + s ≠ 1
[PROOFSTEP]
contrapose! hs'
[GOAL]
s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs' : 1 + s = 1
⊢ s = 0
[PROOFSTEP]
linarith
[GOAL]
case inr.inr.a
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
⊢ log (1 + p * s) < log (1 + s) * p
[PROOFSTEP]
have hs4 : 1 + p * s ≠ 1 := by contrapose! hs'; nlinarith
[GOAL]
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
⊢ 1 + p * s ≠ 1
[PROOFSTEP]
contrapose! hs'
[GOAL]
s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
⊢ s = 0
[PROOFSTEP]
nlinarith
[GOAL]
case inr.inr.a
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ log (1 + p * s) < log (1 + s) * p
[PROOFSTEP]
cases' lt_or_gt_of_ne hs' with hs' hs'
[GOAL]
case inr.inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) < log (1 + s) * p
[PROOFSTEP]
rw [← div_lt_iff hp, ← div_lt_div_right_of_neg hs']
  -- Porting note: previously we could write `zero_lt_one` inline,
      -- but now Lean doesn't guess we are talking about `1` fast enough.
[GOAL]
case inr.inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s < log (1 + p * s) / p / s
[PROOFSTEP]
haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
[GOAL]
case inr.inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
this : 1 ∈ Ioi 0
⊢ log (1 + s) / s < log (1 + p * s) / p / s
[PROOFSTEP]
convert strictConcaveOn_log_Ioi.secant_strict_mono this hs2 hs1 hs4 hs3 _ using 1
[GOAL]
case h.e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
this : 1 ∈ Ioi 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
[PROOFSTEP]
field_simp [log_one]
[GOAL]
case h.e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
this : 1 ∈ Ioi 0
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
[PROOFSTEP]
field_simp [log_one]
[GOAL]
case inr.inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
this : 1 ∈ Ioi 0
⊢ 1 + p * s < 1 + s
[PROOFSTEP]
nlinarith
[GOAL]
case inr.inr.a.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
⊢ log (1 + p * s) < log (1 + s) * p
[PROOFSTEP]
rw [← div_lt_iff hp, ← div_lt_div_right hs']
  -- Porting note: previously we could write `zero_lt_one` inline,
      -- but now Lean doesn't guess we are talking about `1` fast enough.
[GOAL]
case inr.inr.a.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
⊢ log (1 + p * s) / p / s < log (1 + s) / s
[PROOFSTEP]
haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
[GOAL]
case inr.inr.a.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
this : 1 ∈ Ioi 0
⊢ log (1 + p * s) / p / s < log (1 + s) / s
[PROOFSTEP]
convert strictConcaveOn_log_Ioi.secant_strict_mono this hs1 hs2 hs3 hs4 _ using 1
[GOAL]
case h.e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
this : 1 ∈ Ioi 0
⊢ log (1 + p * s) / p / s = (log (1 + p * s) - log 1) / (1 + p * s - 1)
[PROOFSTEP]
field_simp [log_one, hp.ne']
[GOAL]
case h.e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
this : 1 ∈ Ioi 0
⊢ log (1 + s) / s = (log (1 + s) - log 1) / (1 + s - 1)
[PROOFSTEP]
field_simp [log_one]
[GOAL]
case inr.inr.a.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp✝ : 1 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hp : 0 < p
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
this : 1 ∈ Ioi 0
⊢ 1 + s < 1 + p * s
[PROOFSTEP]
nlinarith
[GOAL]
s : ℝ
hs : -1 ≤ s
p : ℝ
hp : 1 ≤ p
⊢ 1 + p * s ≤ (1 + s) ^ p
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | hp)
[GOAL]
case inl
s : ℝ
hs : -1 ≤ s
hp : 1 ≤ 1
⊢ 1 + 1 * s ≤ (1 + s) ^ 1
[PROOFSTEP]
simp
[GOAL]
case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p
[PROOFSTEP]
by_cases hs' : s = 0
[GOAL]
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
[PROOFSTEP]
simp [hs']
[GOAL]
case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
[PROOFSTEP]
exact (one_add_mul_self_lt_rpow_one_add hs hs' hp).le
[GOAL]
p : ℝ
hp : 1 < p
⊢ StrictConvexOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
apply strictConvexOn_of_slope_strict_mono_adjacent (convex_Ici (0 : ℝ))
[GOAL]
p : ℝ
hp : 1 < p
⊢ ∀ {x y z : ℝ}, x ∈ Ici 0 → z ∈ Ici 0 → x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
rintro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have hy : 0 < y := by linarith
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
⊢ 0 < y
[PROOFSTEP]
linarith
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have H1 : y ^ (p - 1 + 1) = y ^ (p - 1) * y := rpow_add_one hy.ne' _
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ (p - 1 + 1) = y ^ (p - 1) * y
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
ring_nf at H1 
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
⊢ (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
trans p * y ^ (p - 1)
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
have h3 : 0 < y - x := by linarith only [hxy]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
⊢ 0 < y - x
[PROOFSTEP]
linarith only [hxy]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
have hyx'' : x / y < 1 := by rwa [div_lt_one hy]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
⊢ x / y < 1
[PROOFSTEP]
rwa [div_lt_one hy]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
have hyx''' : x / y - 1 < 0 := by linarith only [hyx'']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
⊢ x / y - 1 < 0
[PROOFSTEP]
linarith only [hyx'']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
have hyx'''' : 0 ≤ x / y := by positivity
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
⊢ 0 ≤ x / y
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
have hyx''''' : -1 ≤ x / y - 1 := by linarith only [hyx'''']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
⊢ -1 ≤ x / y - 1
[PROOFSTEP]
linarith only [hyx'''']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
have : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1) := by
  linarith [one_add_mul_self_lt_rpow_one_add hyx''''' hyx'''.ne hp]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
⊢ 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
[PROOFSTEP]
linarith [one_add_mul_self_lt_rpow_one_add hyx''''' hyx'''.ne hp]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)
[PROOFSTEP]
rw [div_lt_iff h3, ← div_lt_div_right hy']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
⊢ (y ^ p - x ^ p) / y ^ p < p * y ^ (p - 1) * (y - x) / y ^ p
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
⊢ (y ^ p - x ^ p) / y ^ p = 1 - (1 + (x / y - 1)) ^ p
[PROOFSTEP]
have H : (x / y) ^ p = x ^ p / y ^ p := div_rpow hx hy.le _
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
H : (x / y) ^ p = x ^ p / y ^ p
⊢ (y ^ p - x ^ p) / y ^ p = 1 - (1 + (x / y - 1)) ^ p
[PROOFSTEP]
ring_nf at H ⊢
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
H : (x * y⁻¹) ^ p = x ^ p * (y ^ p)⁻¹
⊢ -(x ^ p * (y ^ p)⁻¹) + y ^ p * (y ^ p)⁻¹ = 1 - (x * y⁻¹) ^ p
[PROOFSTEP]
field_simp [hy.ne', hy'.ne'] at H ⊢
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
H : (x / y) ^ p * y ^ p = x ^ p
⊢ -x ^ p + y ^ p = (1 - (x / y) ^ p) * y ^ p
[PROOFSTEP]
linear_combination H
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
⊢ p * y ^ (p - 1) * (y - x) / y ^ p = -p * (x / y - 1)
[PROOFSTEP]
ring_nf at H1 ⊢
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
⊢ p * y ^ (-1 + p) * y * (y ^ p)⁻¹ - p * y ^ (-1 + p) * x * (y ^ p)⁻¹ = p - p * x * y⁻¹
[PROOFSTEP]
field_simp [hy.ne', hy'.ne']
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
h3 : 0 < y - x
hyx'' : x / y < 1
hyx''' : x / y - 1 < 0
hyx'''' : 0 ≤ x / y
hyx''''' : -1 ≤ x / y - 1
this : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1)
⊢ (p * y ^ (-1 + p) * y - p * y ^ (-1 + p) * x) * y = (p * y - p * x) * y ^ p
[PROOFSTEP]
linear_combination p * (-y + x) * H1
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have hyz' : 0 < z - y := by linarith only [hyz]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
⊢ 0 < z - y
[PROOFSTEP]
linarith only [hyz]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have hyz'' : 1 < z / y := by rwa [one_lt_div hy]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
⊢ 1 < z / y
[PROOFSTEP]
rwa [one_lt_div hy]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have hyz''' : 0 < z / y - 1 := by linarith only [hyz'']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
⊢ 0 < z / y - 1
[PROOFSTEP]
linarith only [hyz'']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have hyz'''' : -1 ≤ z / y - 1 := by linarith only [hyz'']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
⊢ -1 ≤ z / y - 1
[PROOFSTEP]
linarith only [hyz'']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
have : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1 := by
  linarith [one_add_mul_self_lt_rpow_one_add hyz'''' hyz'''.ne' hp]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
⊢ p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
[PROOFSTEP]
linarith [one_add_mul_self_lt_rpow_one_add hyz'''' hyz'''.ne' hp]
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)
[PROOFSTEP]
rw [lt_div_iff hyz', ← div_lt_div_right hy']
[GOAL]
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
⊢ p * y ^ (p - 1) * (z - y) / y ^ p < (z ^ p - y ^ p) / y ^ p
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
⊢ p * y ^ (p - 1) * (z - y) / y ^ p = p * (z / y - 1)
[PROOFSTEP]
ring_nf at H1 ⊢
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
⊢ -(p * y ^ (-1 + p) * y * (y ^ p)⁻¹) + p * y ^ (-1 + p) * z * (y ^ p)⁻¹ = -p + p * z * y⁻¹
[PROOFSTEP]
field_simp [hy.ne', hy'.ne'] at H1 ⊢
[GOAL]
case h.e'_3
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
⊢ (-(p * y ^ (-1 + p) * y * y ^ p) + p * y ^ (-1 + p) * z * y ^ p) * y = (-(p * y) + p * z) * (y ^ p * y ^ p)
[PROOFSTEP]
linear_combination p * (y - z) * y ^ p * H1
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
⊢ (z ^ p - y ^ p) / y ^ p = (1 + (z / y - 1)) ^ p - 1
[PROOFSTEP]
have H : (z / y) ^ p = z ^ p / y ^ p := div_rpow hz hy.le _
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
H : (z / y) ^ p = z ^ p / y ^ p
⊢ (z ^ p - y ^ p) / y ^ p = (1 + (z / y - 1)) ^ p - 1
[PROOFSTEP]
ring_nf at H ⊢
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
H : (z * y⁻¹) ^ p = z ^ p * (y ^ p)⁻¹
⊢ z ^ p * (y ^ p)⁻¹ - y ^ p * (y ^ p)⁻¹ = -1 + (z * y⁻¹) ^ p
[PROOFSTEP]
field_simp [hy.ne', hy'.ne'] at H ⊢
[GOAL]
case h.e'_4
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
H1 : y ^ p = y ^ (-1 + p) * y
hyz' : 0 < z - y
hyz'' : 1 < z / y
hyz''' : 0 < z / y - 1
hyz'''' : -1 ≤ z / y - 1
this : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1
H : (z / y) ^ p * y ^ p = z ^ p
⊢ z ^ p - y ^ p = (-1 + (z / y) ^ p) * y ^ p
[PROOFSTEP]
linear_combination -H
[GOAL]
p : ℝ
hp : 1 ≤ p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | hp)
[GOAL]
case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ 1
[PROOFSTEP]
simpa using convexOn_id (convex_Ici _)
[GOAL]
case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact (strictConvexOn_rpow hp).convexOn
[GOAL]
⊢ StrictConcaveOn ℝ (Iio 0) log
[PROOFSTEP]
refine' ⟨convex_Iio _, _⟩
[GOAL]
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Iio 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Iio 0 → x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
[PROOFSTEP]
rintro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • log x + b • log y < log (a • x + b • y)
[PROOFSTEP]
have hx' : 0 < -x := by linarith
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < -x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ a • log x + b • log y < log (a • x + b • y)
[PROOFSTEP]
have hy' : 0 < -y := by linarith
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ 0 < -y
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ a • log x + b • log y < log (a • x + b • y)
[PROOFSTEP]
have hxy' : -x ≠ -y := by contrapose! hxy; linarith
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ -x ≠ -y
[PROOFSTEP]
contrapose! hxy
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy : -x = -y
⊢ x = y
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y < log (a • x + b • y)
[PROOFSTEP]
calc
  a • log x + b • log y = a • log (-x) + b • log (-y) := by simp_rw [log_neg_eq_log]
  _ < log (a • -x + b • -y) := (strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab)
  _ = log (-(a • x + b • y)) := by congr 1; simp only [Algebra.id.smul_eq_mul]; ring
  _ = _ := by rw [log_neg_eq_log]
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y = a • log (-x) + b • log (-y)
[PROOFSTEP]
simp_rw [log_neg_eq_log]
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (a • -x + b • -y) = log (-(a • x + b • y))
[PROOFSTEP]
congr 1
[GOAL]
case e_x
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • -x + b • -y = -(a • x + b • y)
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul]
[GOAL]
case e_x
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a * -x + b * -y = -(a * x + b * y)
[PROOFSTEP]
ring
[GOAL]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (-(a • x + b • y)) = log (a • x + b • y)
[PROOFSTEP]
rw [log_neg_eq_log]
