English
For 0 < x < π/2, x < tan x.
Русский
Пусть 0 < x < π/2. Тогда x < tan x.
LaTeX
$$$0 < x < \frac{\pi}{2} \Rightarrow x < \tan x$$$
Lean4
/-- For all `0 < x < π/2` we have `x < tan x`.
This is proved by checking that the function `tan x - x` vanishes
at zero and has non-negative derivative. -/
theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x :=
by
let U := Ico 0 (π / 2)
have intU : interior U = Ioo 0 (π / 2) := interior_Ico
have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
have cos_pos {y : ℝ} (hy : y ∈ U) : 0 < cos y := by
exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
have sin_pos {y : ℝ} (hy : y ∈ interior U) : 0 < sin y :=
by
rw [intU] at hy
exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
have tan_cts_U : ContinuousOn tan U :=
by
apply ContinuousOn.mono continuousOn_tan
intro z hz
simp only [mem_setOf_eq]
exact (cos_pos hz).ne'
have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
have deriv_pos (y : ℝ) (hy : y ∈ interior U) : 0 < deriv (fun y' : ℝ => tan y' - y') y :=
by
have := cos_pos (interior_subset hy)
simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
norm_cast
have bd2 : cos y ^ 2 < 1 := by
apply lt_of_le_of_ne y.cos_sq_le_one
rw [cos_sq']
simpa only [Ne, sub_eq_self, sq_eq_zero_iff] using (sin_pos hy).ne'
rwa [lt_inv_comm₀, inv_one]
· exact zero_lt_one
simpa only [sq, mul_self_pos] using this.ne'
have mono := strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
have x_in_U : x ∈ U := ⟨h1.le, h2⟩
simpa only [tan_zero, sub_zero, sub_pos] using mono zero_in_U x_in_U h1
