[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]


[GOAL]
⊢ range arcsin = Icc (-(π / 2)) (π / 2)
[PROOFSTEP]
rw [arcsin, range_comp Subtype.val]
[GOAL]
⊢ Subtype.val '' range (IccExtend arcsin.proof_2 ↑(OrderIso.symm sinOrderIso)) = Icc (-(π / 2)) (π / 2)
[PROOFSTEP]
simp [Icc]
[GOAL]
x : ℝ
⊢ arcsin ↑(projIcc (-1) 1 (_ : -1 ≤ 1) x) = arcsin x
[PROOFSTEP]
rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend, Function.comp_apply]
[GOAL]
x : ℝ
hx : x ∈ Icc (-1) 1
⊢ sin (arcsin x) = x
[PROOFSTEP]
simpa [arcsin, IccExtend_of_mem _ _ hx, -OrderIso.apply_symm_apply] using
  Subtype.ext_iff.1 (sinOrderIso.apply_symm_apply ⟨x, hx⟩)
[GOAL]
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin (arcsin (sin x)) = sin x
[PROOFSTEP]
rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]
[GOAL]
x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin y = x
[PROOFSTEP]
subst y
[GOAL]
x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x
[PROOFSTEP]
exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))
[GOAL]
x : ℝ
hx : 1 ≤ x
⊢ arcsin x = π / 2
[PROOFSTEP]
rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]
[GOAL]
⊢ sin (-(π / 2)) = -1
[PROOFSTEP]
rw [sin_neg, sin_pi_div_two]
[GOAL]
x : ℝ
hx : x ≤ -1
⊢ arcsin x = -(π / 2)
[PROOFSTEP]
rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]
[GOAL]
x : ℝ
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
cases' le_total x (-1) with hx₁ hx₁
[GOAL]
case inl
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
[GOAL]
case inr
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
cases' le_total 1 x with hx₂ hx₂
[GOAL]
case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
[GOAL]
case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
refine' arcsin_eq_of_sin_eq _ _
[GOAL]
case inr.inr.refine'_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x
[PROOFSTEP]
rw [sin_neg, sin_arcsin hx₁ hx₂]
[GOAL]
case inr.inr.refine'_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)
[PROOFSTEP]
exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩
[GOAL]
x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
[GOAL]
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
cases' le_total x (-1) with hx₁ hx₁
[GOAL]
case inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : x ≤ -1
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
simp [arcsin_of_le_neg_one hx₁, hy.1, hx₁.trans (neg_one_le_sin _)]
[GOAL]
case inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
cases' lt_or_le 1 x with hx₂ hx₂
[GOAL]
case inr.inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
simp [arcsin_of_one_le hx₂.le, hy.2.not_le, (sin_le_one y).trans_lt hx₂]
[GOAL]
case inr.inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
exact arcsin_le_iff_le_sin ⟨hx₁, hx₂⟩ (mem_Icc_of_Ico hy)
[GOAL]
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : y ∈ Icc (-1) 1
⊢ x ≤ arcsin y ↔ sin x ≤ y
[PROOFSTEP]
rw [← neg_le_neg_iff, ← arcsin_neg,
  arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg, neg_le_neg_iff]
[GOAL]
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
⊢ x ≤ arcsin y ↔ sin x ≤ y
[PROOFSTEP]
rw [← neg_le_neg_iff, ← arcsin_neg, arcsin_le_iff_le_sin' ⟨neg_le_neg hx.2, neg_lt.2 hx.1⟩, sin_neg, neg_le_neg_iff]
[GOAL]
x y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
⊢ arcsin x = y ↔ x = sin y
[PROOFSTEP]
simp only [le_antisymm_iff, arcsin_le_iff_le_sin' (mem_Ico_of_Ioo hy), le_arcsin_iff_sin_le' (mem_Ioc_of_Ioo hy)]
[GOAL]
x : ℝ
⊢ sin 0 ≤ x ↔ 0 ≤ x
[PROOFSTEP]
rw [sin_zero]
[GOAL]
x : ℝ
⊢ arcsin x = 0 ↔ x = 0
[PROOFSTEP]
simp [le_antisymm_iff]
[GOAL]
x : ℝ
⊢ x < sin (π / 2) ↔ x < 1
[PROOFSTEP]
rw [sin_pi_div_two]
[GOAL]
x : ℝ
⊢ sin (-(π / 2)) < x ↔ -1 < x
[PROOFSTEP]
rw [sin_neg, sin_pi_div_two]
[GOAL]
x : ℝ
⊢ π / 4 ≤ arcsin x ↔ sqrt 2 / 2 ≤ x
[PROOFSTEP]
rw [← sin_pi_div_four, le_arcsin_iff_sin_le']
[GOAL]
x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
[PROOFSTEP]
have := pi_pos
[GOAL]
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
[PROOFSTEP]
constructor
[GOAL]
case left
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4
[PROOFSTEP]
linarith
[GOAL]
case right
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
h : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ sin x ∈ Ioo (-1) 1
[PROOFSTEP]
rwa [mem_Ioo, ← arcsin_lt_pi_div_two, ← neg_pi_div_two_lt_arcsin, arcsin_sin h.1.le h.2.le]
[GOAL]
x : ℝ
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₁ : -1 ≤ x
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : ¬-1 ≤ x ⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₁
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₂ : x ≤ 1
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : -1 ≤ x hx₂ : ¬x ≤ 1 ⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₂
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [← eq_sub_iff_add_eq', ← sqrt_inj (sq_nonneg _) (sub_nonneg.2 (sin_sq_le_one (arcsin x))), sq,
  sqrt_mul_self (cos_arcsin_nonneg _)] at this
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = sqrt (1 - sin (arcsin x) ^ 2)
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [this, sin_arcsin hx₁ hx₂]
[GOAL]
x : ℝ
⊢ tan (arcsin x) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [tan_eq_sin_div_cos, cos_arcsin]
[GOAL]
x : ℝ
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₁ : -1 ≤ x
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : ¬-1 ≤ x ⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
have h : sqrt (1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
[GOAL]
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [h]
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
[PROOFSTEP]
simp
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₂ : x ≤ 1
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : -1 ≤ x hx₂ : ¬x ≤ 1 ⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
have h : sqrt (1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
[GOAL]
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [h]
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
[PROOFSTEP]
simp
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [sin_arcsin hx₁ hx₂]
[GOAL]
x : ℝ
⊢ arcsin x = π / 2 - arccos x
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x ≤ π
[PROOFSTEP]
unfold arccos
[GOAL]
x : ℝ
⊢ π / 2 - arcsin x ≤ π
[PROOFSTEP]
linarith [neg_pi_div_two_le_arcsin x]
[GOAL]
x : ℝ
⊢ 0 ≤ arccos x
[PROOFSTEP]
unfold arccos
[GOAL]
x : ℝ
⊢ 0 ≤ π / 2 - arcsin x
[PROOFSTEP]
linarith [arcsin_le_pi_div_two x]
[GOAL]
x : ℝ
⊢ 0 < arccos x ↔ x < 1
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arccos x) = x
[PROOFSTEP]
rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
[GOAL]
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x
[PROOFSTEP]
rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]
[GOAL]
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - (π / 2 - x) = x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ -(π / 2) ≤ π / 2 - x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - x ≤ π / 2
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π
[PROOFSTEP]
linarith
[GOAL]
case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x
[PROOFSTEP]
linarith
[GOAL]
⊢ arccos 0 = π / 2
[PROOFSTEP]
simp [arccos]
[GOAL]
⊢ arccos 1 = 0
[PROOFSTEP]
simp [arccos]
[GOAL]
⊢ arccos (-1) = π
[PROOFSTEP]
simp [arccos, add_halves]
[GOAL]
x : ℝ
⊢ arccos x = 0 ↔ 1 ≤ x
[PROOFSTEP]
simp [arccos, sub_eq_zero]
[GOAL]
x : ℝ
⊢ arccos x = π / 2 ↔ x = 0
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x = π ↔ x ≤ -1
[PROOFSTEP]
rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
[GOAL]
x : ℝ
⊢ arccos (-x) = π - arccos x
[PROOFSTEP]
rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
[GOAL]
x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0
[PROOFSTEP]
rw [arccos, arcsin_of_one_le hx, sub_self]
[GOAL]
x : ℝ
hx : x ≤ -1
⊢ arccos x = π
[PROOFSTEP]
rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves']
[GOAL]
x : ℝ
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₁ : -1 ≤ x
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : ¬-1 ≤ x ⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₁
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₂ : x ≤ 1
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : -1 ≤ x hx₂ : ¬x ≤ 1 ⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₂
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]
[GOAL]
x : ℝ
⊢ arccos x ≤ π / 2 ↔ 0 ≤ x
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x < π / 2 ↔ 0 < x
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x ≤ π / 4 ↔ sqrt 2 / 2 ≤ x
[PROOFSTEP]
rw [arccos, ← pi_div_four_le_arcsin]
[GOAL]
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
[PROOFSTEP]
constructor
[GOAL]
case mp
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x
[PROOFSTEP]
intro
[GOAL]
case mp
x : ℝ
a✝ : π / 2 - arcsin x ≤ π / 4
⊢ π / 4 ≤ arcsin x
[PROOFSTEP]
linarith
[GOAL]
case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
[PROOFSTEP]
intro
[GOAL]
case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ tan (arccos x) = sqrt (1 - x ^ 2) / x
[PROOFSTEP]
rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos (sqrt (1 - x ^ 2))
[PROOFSTEP]
rw [eq_comm, ← cos_arcsin]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x
[PROOFSTEP]
exact arccos_cos (arcsin_nonneg.2 h) ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))


[GOAL]
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
⊢ arg ↑(↑expMapCircle x) = x
[PROOFSTEP]
rw [expMapCircle_apply, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]
[GOAL]
x y : ℝ
⊢ ↑expMapCircle x = ↑expMapCircle y ↔ ∃ m, x = y + ↑m * (2 * π)
[PROOFSTEP]
rw [Subtype.ext_iff, expMapCircle_apply, expMapCircle_apply, exp_eq_exp_iff_exists_int]
[GOAL]
x y : ℝ
⊢ (∃ n, ↑x * I = ↑y * I + ↑n * (2 * ↑π * I)) ↔ ∃ m, x = y + ↑m * (2 * π)
[PROOFSTEP]
refine' exists_congr fun n => _
[GOAL]
x y : ℝ
n : ℤ
⊢ ↑x * I = ↑y * I + ↑n * (2 * ↑π * I) ↔ x = y + ↑n * (2 * π)
[PROOFSTEP]
rw [← mul_assoc, ← add_mul, mul_left_inj' I_ne_zero]
[GOAL]
x y : ℝ
n : ℤ
⊢ ↑x = ↑y + ↑n * (2 * ↑π) ↔ x = y + ↑n * (2 * π)
[PROOFSTEP]
norm_cast
[GOAL]
z : ℝ
⊢ z + 2 * π = z + ↑1 * (2 * π)
[PROOFSTEP]
rw [Int.cast_one, one_mul]
[GOAL]
θ : Angle
⊢ ↑(expMapCircle θ) = ↑(cos θ) + ↑(sin θ) * I
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ ↑(expMapCircle ↑x✝) = ↑(cos ↑x✝) + ↑(sin ↑x✝) * I
[PROOFSTEP]
simp [Complex.exp_mul_I]
[GOAL]
⊢ expMapCircle 0 = 1
[PROOFSTEP]
rw [← Real.Angle.coe_zero, Real.Angle.expMapCircle_coe, _root_.expMapCircle_zero]
[GOAL]
θ : Angle
⊢ expMapCircle (-θ) = (expMapCircle θ)⁻¹
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ expMapCircle (-↑x✝) = (expMapCircle ↑x✝)⁻¹
[PROOFSTEP]
simp_rw [← Real.Angle.coe_neg, Real.Angle.expMapCircle_coe, _root_.expMapCircle_neg]
[GOAL]
θ₁ θ₂ : Angle
⊢ expMapCircle (θ₁ + θ₂) = expMapCircle θ₁ * expMapCircle θ₂
[PROOFSTEP]
induction θ₁ using Real.Angle.induction_on
[GOAL]
case h
θ₂ : Angle
x✝ : ℝ
⊢ expMapCircle (↑x✝ + θ₂) = expMapCircle ↑x✝ * expMapCircle θ₂
[PROOFSTEP]
induction θ₂ using Real.Angle.induction_on
[GOAL]
case h.h
x✝¹ x✝ : ℝ
⊢ expMapCircle (↑x✝¹ + ↑x✝) = expMapCircle ↑x✝¹ * expMapCircle ↑x✝
[PROOFSTEP]
exact _root_.expMapCircle_add _ _
[GOAL]
θ : Angle
⊢ ↑(arg ↑(expMapCircle θ)) = θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ ↑(arg ↑(expMapCircle ↑x✝)) = ↑x✝
[PROOFSTEP]
rw [Real.Angle.expMapCircle_coe, expMapCircle_apply, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ← Real.Angle.cos_coe, ←
  Real.Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]


[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
n : ℕ
⊢ ↑(aeval x) (T R n) = eval x (T A n)
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, map_T]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
n : ℕ
⊢ ↑(aeval x) (U R n) = eval x (U A n)
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, map_U]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : R
n : ℕ
⊢ ↑(algebraMap R A) (eval x (T R n)) = eval (↑(algebraMap R A) x) (T A n)
[PROOFSTEP]
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : R
n : ℕ
⊢ ↑(algebraMap R A) (eval x (U R n)) = eval (↑(algebraMap R A) x) (U A n)
[PROOFSTEP]
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (T ℂ 0) = cos (↑0 * θ)
[PROOFSTEP]
simp only [T_zero, eval_one, Nat.cast_zero, zero_mul, cos_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (T ℂ 1) = cos (↑1 * θ)
[PROOFSTEP]
simp only [eval_X, one_mul, T_one, Nat.cast_one]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
[PROOFSTEP]
have : (2 : ℂ[X]) = (2 : ℕ) := by norm_num
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ 2 = ↑2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
[PROOFSTEP]
simp only [this, eval_X, eval_one, T_add_two, eval_sub, eval_mul, eval_nat_cast]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ ↑2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos (↑(n + 2) * θ)
[PROOFSTEP]
simp only [Nat.cast_ofNat, Nat.cast_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos ((↑n + 2) * θ)
[PROOFSTEP]
rw [T_complex_cos (n + 1), T_complex_cos n]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * cos (↑(n + 1) * θ) - cos (↑n * θ) = cos ((↑n + 2) * θ)
[PROOFSTEP]
simp only [Nat.cast_add, Nat.cast_one, add_mul, cos_add, one_mul, mul_assoc, sin_two_mul, cos_two_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * (cos θ * (cos (↑n * θ) * cos θ - sin (↑n * θ) * sin θ)) - cos (↑n * θ) =
    cos (↑n * θ) * (2 * cos θ ^ 2 - 1) - sin (↑n * θ) * (2 * (sin θ * cos θ))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (U ℂ Nat.zero) * sin θ = sin ((↑Nat.zero + 1) * θ)
[PROOFSTEP]
simp [U_zero, eval_one, zero_add, one_mul, Nat.zero_eq, CharP.cast_eq_zero]
[GOAL]
case succ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ eval (cos θ) (U ℂ (Nat.succ d)) * sin θ = sin ((↑(Nat.succ d) + 1) * θ)
[PROOFSTEP]
rw [U_eq_X_mul_U_add_T]
[GOAL]
case succ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ eval (cos θ) (X * U ℂ d + T ℂ (d + 1)) * sin θ = sin ((↑(Nat.succ d) + 1) * θ)
[PROOFSTEP]
simp only [eval_add, eval_mul, eval_X, T_complex_cos, add_mul, mul_assoc, hd, one_mul]
  -- Porting note: added `trans` to prevent `rw` from going on a wild goose chase applying `rfl`
[GOAL]
case succ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos (↑(d + 1) * θ) * sin θ = sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
trans cos θ * sin (↑(d.succ) * θ) + cos (↑(d.succ) * θ) * sin θ
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos (↑(d + 1) * θ) * sin θ =
    cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ = sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
swap
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ = sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
conv_rhs => rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
| sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
| sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
| sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos (↑(d + 1) * θ) * sin θ =
    cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ
[PROOFSTEP]
push_cast
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos ((↑d + 1) * θ) * sin θ = cos θ * sin ((↑d + 1) * θ) + cos ((↑d + 1) * θ) * sin θ
[PROOFSTEP]
simp only [add_mul, one_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℝ
n : ℕ
⊢ eval (cos θ) (T ℝ n) = cos (↑n * θ)
[PROOFSTEP]
exact_mod_cast T_complex_cos θ n
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℝ
n : ℕ
⊢ eval (cos θ) (U ℝ n) * sin θ = sin ((↑n + 1) * θ)
[PROOFSTEP]
exact_mod_cast U_complex_cos θ n


[GOAL]
θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 :=
  by
  rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul, add_eq_zero_iff_eq_neg,
    neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]
  congr 3; ring_nf
[GOAL]
θ : ℂ
⊢ (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
[PROOFSTEP]
rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul, add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul,
  ← div_eq_iff (exp_ne_zero _), ← exp_sub]
[GOAL]
θ : ℂ
⊢ exp (θ * I - -θ * I) = -1 ↔ exp (2 * θ * I) = -1
[PROOFSTEP]
congr 3
[GOAL]
θ : ℂ
⊢ exp (θ * I - -θ * I) = -1 ↔ exp (2 * θ * I) = -1
[PROOFSTEP]
ring_nf
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
⊢ (∃ n, 2 * I * θ = ↑π * I + ↑n * (2 * ↑π * I)) ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
refine' exists_congr fun x => _
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2
[PROOFSTEP]
refine' (iff_of_eq <| congr_arg _ _).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
x : ℤ
⊢ ↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)
[PROOFSTEP]
field_simp
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
x : ℤ
⊢ (↑π * I + ↑x * (2 * ↑π * I)) * 2 = 2 * I * ((2 * ↑x + 1) * ↑π)
[PROOFSTEP]
ring
[GOAL]
θ : ℂ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
rw [← not_exists, not_iff_not, cos_eq_zero_iff]
[GOAL]
θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
rw [← Complex.cos_sub_pi_div_two, cos_eq_zero_iff]
[GOAL]
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) ↔ ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
constructor
[GOAL]
case mp
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) → ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mp.intro
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
use k + 1
[GOAL]
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ θ = ↑(k + 1) * ↑π
[PROOFSTEP]
field_simp [eq_add_of_sub_eq hk]
[GOAL]
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ (2 * ↑k + 1) * ↑π + ↑π = (↑k + 1) * ↑π * 2
[PROOFSTEP]
ring
[GOAL]
case mpr
θ : ℂ
⊢ (∃ k, θ = ↑k * ↑π) → ∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case mpr.intro
k : ℤ
⊢ ∃ k_1, ↑k * ↑π - ↑π / 2 = (2 * ↑k_1 + 1) * ↑π / 2
[PROOFSTEP]
use k - 1
[GOAL]
case h
k : ℤ
⊢ ↑k * ↑π - ↑π / 2 = (2 * ↑(k - 1) + 1) * ↑π / 2
[PROOFSTEP]
field_simp
[GOAL]
case h
k : ℤ
⊢ ↑k * ↑π * 2 - ↑π = (2 * (↑k - 1) + 1) * ↑π
[PROOFSTEP]
ring
[GOAL]
θ : ℂ
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π
[PROOFSTEP]
rw [← not_exists, not_iff_not, sin_eq_zero_iff]
[GOAL]
θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
have h := (sin_two_mul θ).symm
[GOAL]
θ : ℂ
h : 2 * sin θ * cos θ = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
rw [mul_assoc] at h
[GOAL]
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
rw [tan, div_eq_zero_iff, ← mul_eq_zero, ← zero_mul (1 / 2 : ℂ), mul_one_div,
  CancelDenoms.cancel_factors_eq_div h two_ne_zero, mul_comm]
[GOAL]
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ sin (θ * 2) / 2 = 0 / 2 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
simpa only [zero_div, zero_mul, Ne.def, not_false_iff, field_simps] using sin_eq_zero_iff
[GOAL]
θ : ℂ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π / 2
[PROOFSTEP]
rw [← not_exists, not_iff_not, tan_eq_zero_iff]
[GOAL]
n : ℤ
⊢ ∃ k, ↑n * ↑π / 2 = ↑k * ↑π / 2
[PROOFSTEP]
use n
[GOAL]
x y : ℂ
⊢ cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
[PROOFSTEP]
rw [cos_sub_cos]
[GOAL]
x y : ℂ
⊢ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ sin ((x + y) / 2) = 0 ∨ sin ((x - y) / 2) = 0
[PROOFSTEP]
simp [(by norm_num : (2 : ℂ) ≠ 0)]
[GOAL]
x y : ℂ
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 ↔ (∃ k, y = 2 * ↑k * ↑π + x) ∨ ∃ k, y = 2 * ↑k * ↑π - x
[PROOFSTEP]
apply or_congr
[GOAL]
case h₁
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π + x
[PROOFSTEP]
field_simp [sin_eq_zero_iff, (by norm_num : -(2 : ℂ) ≠ 0), eq_sub_iff_add_eq', sub_eq_iff_eq_add, mul_comm (2 : ℂ),
  mul_right_comm _ (2 : ℂ)]
[GOAL]
x y : ℂ
⊢ -2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case h₂
x y : ℂ
⊢ sin ((x + y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π - x
[PROOFSTEP]
field_simp [sin_eq_zero_iff, (by norm_num : -(2 : ℂ) ≠ 0), eq_sub_iff_add_eq', sub_eq_iff_eq_add, mul_comm (2 : ℂ),
  mul_right_comm _ (2 : ℂ)]
[GOAL]
x y : ℂ
⊢ -2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case h₁
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) ↔ ∃ k, y = ↑k * ↑π * 2 + x
[PROOFSTEP]
constructor
[GOAL]
case h₁.mp
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) → ∃ k, y = ↑k * ↑π * 2 + x
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case h₁.mp.intro
y : ℂ
k : ℤ
⊢ ∃ k_1, y = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + y)
[PROOFSTEP]
use-k
[GOAL]
case h
y : ℂ
k : ℤ
⊢ y = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + y)
[PROOFSTEP]
simp
[GOAL]
case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case h₁.mpr.intro
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)
[PROOFSTEP]
use-k
[GOAL]
case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)
[PROOFSTEP]
simp
[GOAL]
x y : ℂ
⊢ sin x = sin y ↔ ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]
[GOAL]
x y : ℂ
⊢ (∃ k, y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ∨ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2) ↔
    ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
refine' exists_congr fun k => or_congr _ _
[GOAL]
case refine'_1
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ↔ y = 2 * ↑k * ↑π + x
[PROOFSTEP]
refine' Eq.congr rfl _
[GOAL]
case refine'_2
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 ↔ y = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
refine' Eq.congr rfl _
[GOAL]
case refine'_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 = 2 * ↑k * ↑π + x
[PROOFSTEP]
field_simp
[GOAL]
case refine'_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
field_simp
[GOAL]
case refine'_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π * 2 + (x * 2 - ↑π) + ↑π = (2 * ↑k * ↑π + x) * 2
[PROOFSTEP]
ring
[GOAL]
case refine'_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π * 2 - (x * 2 - ↑π) + ↑π = ((2 * ↑k + 1) * ↑π - x) * 2
[PROOFSTEP]
ring
[GOAL]
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)
[GOAL]
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
rw [tan, sin_add, cos_add, ←
  div_div_div_cancel_right (sin x * cos y + cos x * sin y)
    (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)),
  add_div, sub_div]
[GOAL]
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
simp only [← div_mul_div_comm, tan, mul_one, one_mul, div_self (cos_ne_zero_iff.mpr h1),
  div_self (cos_ne_zero_iff.mpr h2)]
[GOAL]
case inr.intro.intro.intro
k l : ℤ
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
haveI t := tan_int_mul_pi_div_two
[GOAL]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
[GOAL]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan (↑(2 * k + 1) * ↑π / 2) = 0
hy : tan (↑(2 * l + 1) * ↑π / 2) = 0
hxy : tan (↑(2 * k + 1 + (2 * l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one, hx, hy] at hx hy hxy
[GOAL]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
rw [hx, hy, add_zero, zero_div, mul_div_assoc, mul_div_assoc, ← add_mul (2 * (k : ℂ) + 1) (2 * l + 1) (π / 2), ←
  mul_div_assoc, hxy]
[GOAL]
z : ℂ
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
by_cases h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
[GOAL]
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
[GOAL]
case neg
z : ℂ
h : ¬∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
rw [not_forall_not] at h
[GOAL]
case neg
z : ℂ
h : ∃ x, z = (2 * ↑x + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]
[GOAL]
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
[PROOFSTEP]
rw [tan_add h, tan_mul_I, mul_assoc]
[GOAL]
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan z = (tan ↑z.re + tanh ↑z.im * I) / (1 - tan ↑z.re * tanh ↑z.im * I)
[PROOFSTEP]
convert tan_add_mul_I h
[GOAL]
case h.e'_2.h.e'_1
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I
[PROOFSTEP]
exact (re_add_im z).symm
[GOAL]
z w : ℂ
⊢ cos z = w ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
z w : ℂ
⊢ cos z - w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
[PROOFSTEP]
field_simp [cos, exp_neg, exp_ne_zero]
[GOAL]
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
[PROOFSTEP]
refine' Eq.congr _ rfl
[GOAL]
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1
[PROOFSTEP]
ring
[GOAL]
⊢ Function.Surjective cos
[PROOFSTEP]
intro x
[GOAL]
x : ℂ
⊢ ∃ a, cos a = x
[PROOFSTEP]
obtain ⟨w, w₀, hw⟩ : ∃ (w : _) (_ : w ≠ 0), 1 * w * w + -2 * x * w + 1 = 0 :=
  by
  rcases exists_quadratic_eq_zero one_ne_zero ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with ⟨w, hw⟩
  refine' ⟨w, _, hw⟩
  rintro rfl
  simp only [zero_add, one_ne_zero, mul_zero] at hw
[GOAL]
x : ℂ
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
[PROOFSTEP]
rcases exists_quadratic_eq_zero one_ne_zero ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with ⟨w, hw⟩
[GOAL]
case intro
x w : ℂ
hw : 1 * w * w + ?m.63171 * w + ?m.63172 = 0
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
[PROOFSTEP]
refine' ⟨w, _, hw⟩
[GOAL]
case intro
x w : ℂ
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro
x : ℂ
hw : 1 * 0 * 0 + -2 * x * 0 + 1 = 0
⊢ False
[PROOFSTEP]
simp only [zero_add, one_ne_zero, mul_zero] at hw
[GOAL]
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ ∃ a, cos a = x
[PROOFSTEP]
refine' ⟨log w / I, cos_eq_iff_quadratic.2 _⟩
[GOAL]
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ exp (log w / I * I) ^ 2 - 2 * x * exp (log w / I * I) + 1 = 0
[PROOFSTEP]
rw [div_mul_cancel _ I_ne_zero, exp_log w₀]
[GOAL]
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0
[PROOFSTEP]
convert hw using 1
[GOAL]
case h.e'_2
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 1 * w * w + -2 * x * w + 1
[PROOFSTEP]
ring
[GOAL]
⊢ Function.Surjective sin
[PROOFSTEP]
intro x
[GOAL]
x : ℂ
⊢ ∃ a, sin a = x
[PROOFSTEP]
rcases cos_surjective x with ⟨z, rfl⟩
[GOAL]
case intro
z : ℂ
⊢ ∃ a, sin a = cos z
[PROOFSTEP]
exact ⟨z + π / 2, sin_add_pi_div_two z⟩
[GOAL]
θ : ℝ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * π / 2
[PROOFSTEP]
exact_mod_cast @Complex.cos_eq_zero_iff θ
[GOAL]
θ : ℝ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * π / 2
[PROOFSTEP]
rw [← not_exists, not_iff_not, cos_eq_zero_iff]
[GOAL]
x y : ℝ
⊢ cos x = cos y ↔ ∃ k, y = 2 * ↑k * π + x ∨ y = 2 * ↑k * π - x
[PROOFSTEP]
exact_mod_cast @Complex.cos_eq_cos_iff x y
[GOAL]
x y : ℝ
⊢ sin x = sin y ↔ ∃ k, y = 2 * ↑k * π + x ∨ y = (2 * ↑k + 1) * π - x
[PROOFSTEP]
exact_mod_cast @Complex.sin_eq_sin_iff x y
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)
[PROOFSTEP]
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩ pi_div_two_pos.ne
    (sub_pos.2 hx') hx
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ 1
⊢ x ≤ sin (π / 2 * x)
[PROOFSTEP]
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.concaveOn.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩ (sub_nonneg.2 hx')
    hx
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ 2 / π * x < sin x
[PROOFSTEP]
rw [← inv_div]
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x
[PROOFSTEP]
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using
  @lt_sin_mul ((π / 2)⁻¹ * x) (mul_pos (inv_pos.2 pi_div_two_pos) hx)
    (by rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos])
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < 1
[PROOFSTEP]
rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos]
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ 2 / π * x ≤ sin x
[PROOFSTEP]
rw [← inv_div]
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x
[PROOFSTEP]
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using
  @le_sin_mul ((π / 2)⁻¹ * x) (mul_nonneg (inv_nonneg.2 pi_div_two_pos.le) hx)
    (by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos])
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1
[PROOFSTEP]
rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos]


[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) (cos z)
[PROOFSTEP]
rw [Complex.cos, Complex.exp_eq_exp_ℂ]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
have := ((expSeries_div_hasSum_exp ℂ (z * Complex.I)).add (expSeries_div_hasSum_exp ℂ (-z * Complex.I))).div_const 2
[GOAL]
z : ℂ
this :
  HasSum (fun i => ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
[GOAL]
z : ℂ
this :
  HasSum ((fun i => ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ∘ ↑(Nat.divModEquiv 2).symm)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)! +
          (-z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
simp_rw [← mul_comm 2 _] at this
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
refine' this.prod_fiberwise fun k => _
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ HasSum
    (fun c =>
      ((z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)! +
          (-z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)!) /
        2)
    ((z * I) ^ (2 * k) / ↑(2 * k)!)
[PROOFSTEP]
dsimp only
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ HasSum (fun c => ((z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)! + (-z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)!) / 2)
    ((z * I) ^ (2 * k) / ↑(2 * k)!)
[PROOFSTEP]
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    Finset.sum Finset.univ fun b =>
      ((z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)! + (-z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)!) / 2
[PROOFSTEP]
rw [Fin.sum_univ_two]
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! + (-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) / 2 +
      ((z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! + (-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) / 2
[PROOFSTEP]
simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ', pow_mul, mul_pow, neg_sq, ← two_mul, neg_mul, mul_neg, neg_div,
  add_right_neg, zero_div, add_zero, mul_div_cancel_left _ (two_ne_zero : (2 : ℂ) ≠ 0)]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) (sin z)
[PROOFSTEP]
rw [Complex.sin, Complex.exp_eq_exp_ℂ]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
have :=
  (((expSeries_div_hasSum_exp ℂ (-z * Complex.I)).sub (expSeries_div_hasSum_exp ℂ (z * Complex.I))).mul_right
        Complex.I).div_const
    2
[GOAL]
z : ℂ
this :
  HasSum (fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
[GOAL]
z : ℂ
this :
  HasSum ((fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2) ∘ ↑(Nat.divModEquiv 2).symm)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)! -
            (z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
simp_rw [← mul_comm 2 _] at this
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
refine' this.prod_fiberwise fun k => _
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ HasSum
    (fun c =>
      ((-z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)! -
            (z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)!) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I)
[PROOFSTEP]
dsimp only
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ HasSum (fun c => ((-z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)! - (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)!) * I / 2)
    ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I)
[PROOFSTEP]
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    Finset.sum Finset.univ fun b =>
      ((-z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)! - (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)!) * I / 2
[PROOFSTEP]
rw [Fin.sum_univ_two]
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    ((-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! - (z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) * I / 2 +
      ((-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! - (z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) * I / 2
[PROOFSTEP]
simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ', pow_mul, mul_pow, neg_sq, sub_self, zero_mul, zero_div,
  zero_add, neg_mul, mul_neg, neg_div, ← neg_add', ← two_mul, neg_mul, neg_div, mul_assoc,
  mul_div_cancel_left _ (two_ne_zero : (2 : ℂ) ≠ 0), Complex.div_I]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (cos z)
[PROOFSTEP]
convert Complex.hasSum_cos' z using 1
[GOAL]
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!
[PROOFSTEP]
simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin z)
[PROOFSTEP]
convert Complex.hasSum_sin' z using 1
[GOAL]
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I
[PROOFSTEP]
simp_rw [mul_pow, pow_succ', pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
  div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
[GOAL]
r : ℝ
⊢ HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(2 * n)!) (cos r)
[PROOFSTEP]
exact_mod_cast Complex.hasSum_cos r
[GOAL]
r : ℝ
⊢ HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin r)
[PROOFSTEP]
exact_mod_cast Complex.hasSum_sin r