case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x => x ^ m) (Ioi 0)

case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ (x : ℝ), x ∈ Ioi 0 → 0 < (deriv^[2]) (fun x => x ^ m) x
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (Ioi 0) fun x => x ^ m
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < (deriv^[2]) (fun x => x ^ m) x
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ (x : ℝ), x ∈ Ioi 0 → 0 < (deriv^[2]) (fun x => x ^ m) x
intro x hx
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (deriv^[2]) (fun x => x ^ m) x
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < (deriv^[2]) (fun x => x ^ m) x
rw [mem_Ioi] at hx
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i in Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (deriv^[2]) (fun x => x ^ m) x
rw [iter_deriv_zpow]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (↑m - ↑i)
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i in Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)
refine' mul_pos _ (zpow_pos_of_pos hx _)
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (m - ↑i)
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (↑m - ↑i)
norm_cast
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Ico 0 ↑2
⊢ False
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (m - ↑i)
refine' int_prod_range_pos (by simp only) fun hm => _
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
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Ico 0 ↑2
⊢ False
rw [← Finset.coe_Ico] at hm
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
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
norm_cast at hm
no goals
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
fin_cases hm <;> simp_all
no goals
case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x => x ^ m) (Ioi 0)
exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx
no goals
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ Even 2
simp only