[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ StrictConvexOn ℝ (Ici 0) fun x => x ^ n
[PROOFSTEP]
apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _)
[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (deriv fun x => x ^ n) (interior (Ici 0))
[PROOFSTEP]
rw [deriv_pow', interior_Ici]
[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (fun x => ↑n * x ^ (n - 1)) (Ioi 0)
[PROOFSTEP]
exact fun x (hx : 0 < x) y hy hxy =>
  mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_left hxy hx.le <| Nat.sub_pos_of_lt hn)
    (Nat.cast_pos.2 <| zero_lt_two.trans_le hn)
[GOAL]
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictConvexOn ℝ univ fun x => x ^ n
[PROOFSTEP]
apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)
[GOAL]
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a => a ^ n)
[PROOFSTEP]
rw [deriv_pow']
[GOAL]
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
[PROOFSTEP]
replace h := Nat.pos_of_ne_zero h
[GOAL]
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
[PROOFSTEP]
exact StrictMono.const_mul (Odd.strictMono_pow <| Nat.Even.sub_odd h hn <| Nat.odd_iff.2 rfl) (Nat.cast_pos.2 h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : f x ≤ 0
⊢ 0 ≤ -1 * f x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : ¬f x ≤ 0
⊢ 0 ≤ 1 * f x
[PROOFSTEP]
simp at hx ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x
[PROOFSTEP]
exact le_of_lt hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
⊢ ∏ x in s, (if f x ≤ 0 then -1 else 1) * f x = ∏ x in s, f x
[PROOFSTEP]
rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one, Finset.prod_const,
  neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
[GOAL]
m : ℤ
n : ℕ
hn : Even n
⊢ 0 ≤ ∏ k in Finset.range n, (m - ↑k)
[PROOFSTEP]
rcases hn with ⟨n, rfl⟩
[GOAL]
case intro
m : ℤ
n : ℕ
⊢ 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case intro.zero
m : ℤ
⊢ 0 ≤ ∏ k in Finset.range (Nat.zero + Nat.zero), (m - ↑k)
[PROOFSTEP]
simp
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
[PROOFSTEP]
rw [← two_mul] at ihn 
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
[PROOFSTEP]
rw [← two_mul, Nat.succ_eq_add_one, mul_add, mul_one, ← one_add_one_eq_two, ← add_assoc, Finset.prod_range_succ,
  Finset.prod_range_succ, mul_assoc]
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (∏ x in Finset.range ((1 + 1) * n), (m - ↑x)) * ((m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1)))
[PROOFSTEP]
refine' mul_nonneg ihn _
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))
[PROOFSTEP]
generalize (1 + 1) * n = k
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
cases' le_or_lt m k with hmk hmk
[GOAL]
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
have : m ≤ k + 1 := hmk.trans (lt_add_one (k : ℤ)).le
[GOAL]
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
convert mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _
[GOAL]
case intro.succ.inl.convert_2
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ m - ↑(k + 1) ≤ 0
[PROOFSTEP]
convert sub_nonpos_of_le this
[GOAL]
case intro.succ.inr
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : ↑k < m
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
exact mul_nonneg (sub_nonneg_of_le hmk.le) (sub_nonneg_of_le hmk)
[GOAL]
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
⊢ 0 < ∏ k in Finset.range n, (m - ↑k)
[PROOFSTEP]
refine' (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm _
[GOAL]
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : 0 = ∏ k in Finset.range n, (m - ↑k)
⊢ m ∈ Ico 0 ↑n
[PROOFSTEP]
rw [eq_comm, Finset.prod_eq_zero_iff] at h 
[GOAL]
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : ∃ a, a ∈ Finset.range n ∧ m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
[PROOFSTEP]
obtain ⟨a, ha, h⟩ := h
[GOAL]
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
[PROOFSTEP]
rw [sub_eq_zero.1 h]
[GOAL]
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n
[PROOFSTEP]
exact ⟨Int.ofNat_zero_le _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩
[GOAL]
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (Ioi 0) fun x => x ^ m
[PROOFSTEP]
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
[GOAL]
case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x => x ^ m) (Ioi 0)
[PROOFSTEP]
exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ (x : ℝ), x ∈ Ioi 0 → 0 < deriv^[2] (fun x => x ^ m) x
[PROOFSTEP]
intro x hx
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv^[2] (fun x => x ^ m) x
[PROOFSTEP]
rw [mem_Ioi] at hx 
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x => x ^ m) x
[PROOFSTEP]
rw [iter_deriv_zpow]
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i in Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)
[PROOFSTEP]
refine' mul_pos _ (zpow_pos_of_pos hx _)
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (↑m - ↑i)
[PROOFSTEP]
norm_cast
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (m - ↑i)
[PROOFSTEP]
refine' int_prod_range_pos (by simp only) fun hm => _
[GOAL]
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ Even 2
[PROOFSTEP]
simp only
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Ico 0 ↑2
⊢ False
[PROOFSTEP]
rw [← Finset.coe_Ico] at hm 
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm✝ : m ∈ Ico 0 ↑2
hm : m ∈ ↑(Finset.Ico 0 ↑2)
⊢ False
[PROOFSTEP]
norm_cast at hm 
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm✝ : m ∈ Ico 0 ↑2
hm : m ∈ Finset.Ico 0 2
⊢ False
[PROOFSTEP]
fin_cases hm
[GOAL]
case hf''.head
x : ℝ
hx : 0 < x
hm₀ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 0 ≠ 0
hm₁ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 0 ≠ 1
hm : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 0 ∈ Ico 0 ↑2
⊢ False
[PROOFSTEP]
simp_all
  -- Porting note: `simp_all` was `cc`
[GOAL]
case hf''.tail.head
x : ℝ
hx : 0 < x
hm₀ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 1 ≠ 0
hm₁ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 1 ≠ 1
hm : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 1 ∈ Ico 0 ↑2
⊢ False
[PROOFSTEP]
simp_all
  -- Porting note: `simp_all` was `cc`
[GOAL]
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x => sqrt x * log x) ((2 + log x) / (2 * sqrt x)) x
[PROOFSTEP]
convert (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1
[GOAL]
case h.e'_7
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * sqrt x) = 1 / (2 * sqrt x) * log x + sqrt x * x⁻¹
[PROOFSTEP]
rw [add_div, div_mul_right (sqrt x) two_ne_zero, ← div_eq_mul_inv, sqrt_div_self', add_comm, div_eq_mul_one_div,
  mul_comm]
[GOAL]
x : ℝ
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
[PROOFSTEP]
cases' lt_or_le 0 x with hx hx
[GOAL]
case inl
x : ℝ
hx : 0 < x
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
[PROOFSTEP]
exact (hasDerivAt_sqrt_mul_log hx.ne').deriv
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = 0
[PROOFSTEP]
refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => sqrt x * log x) 0 (Iic 0) x
[PROOFSTEP]
refine' (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => _) hx
[GOAL]
case inr
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ sqrt x * log x = 0
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, zero_mul]
[GOAL]
x : ℝ
⊢ deriv^[2] (fun x => sqrt x * log x) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
simp only [Nat.iterate, deriv_sqrt_mul_log']
[GOAL]
x : ℝ
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
cases' le_or_lt x 0 with hx hx
[GOAL]
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, zero_pow zero_lt_three, mul_zero, div_zero]
[GOAL]
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = 0
[PROOFSTEP]
refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
[GOAL]
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => (2 + log x) / (2 * sqrt x)) 0 (Iic 0) x
[PROOFSTEP]
refine' (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => _) hx
[GOAL]
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * sqrt x) = 0
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
[GOAL]
case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
have h₀ : sqrt x ≠ 0 := sqrt_ne_zero'.2 hx
[GOAL]
case inr
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
convert
  (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
      mul_ne_zero two_ne_zero h₀).deriv using
  1
[GOAL]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) = (x⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
[PROOFSTEP]
nth_rw 3 [← mul_self_sqrt hx.le]
[GOAL]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) =
    ((sqrt x * sqrt x)⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -(log x * (sqrt x * sqrt x * (2 * sqrt x) * (2 * sqrt x) ^ 2)) =
    (2 * sqrt x * (2 * sqrt x) - sqrt x * sqrt x * ((2 + log x) * 2)) * (4 * sqrt x ^ 3)
[PROOFSTEP]
ring
[GOAL]
⊢ StrictConcaveOn ℝ (Ioi 1) fun x => sqrt x * log x
[PROOFSTEP]
apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_
[GOAL]
⊢ ContinuousOn (fun x => sqrt x * log x) (Ioi 1)
[PROOFSTEP]
exact continuous_sqrt.continuousOn.mul (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))
[GOAL]
x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x => sqrt x * log x) x < 0
[PROOFSTEP]
rw [deriv2_sqrt_mul_log x]
[GOAL]
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (↑4 * sqrt x ^ 3) < 0
[PROOFSTEP]
exact
  div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
    (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))
[GOAL]
⊢ StrictConcaveOn ℝ (Icc 0 π) sin
[PROOFSTEP]
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_
[GOAL]
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ deriv^[2] sin x < 0
[PROOFSTEP]
rw [interior_Icc] at hx 
[GOAL]
x : ℝ
hx : x ∈ Ioo 0 π
⊢ deriv^[2] sin x < 0
[PROOFSTEP]
simp [sin_pos_of_mem_Ioo hx]
[GOAL]
⊢ StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos
[PROOFSTEP]
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_cos fun x hx => ?_
[GOAL]
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ deriv^[2] cos x < 0
[PROOFSTEP]
rw [interior_Icc] at hx 
[GOAL]
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ deriv^[2] cos x < 0
[PROOFSTEP]
simp [cos_pos_of_mem_Ioo hx]
