English
For all x with -(3π/2) ≤ x ≤ 3π/2 and x ≠ 0, cos x < 1/√(x^2+1).
Русский
Для всех x с -(3π/2) ≤ x ≤ 3π/2 и x ≠ 0 верно cos x < 1/√(x^2+1).
LaTeX
$$$\forall x \in \mathbb{R}, -(\tfrac{3\pi}{2}) \le x \le (\tfrac{3\pi}{2}) \\ x \ne 0 \Rightarrow \cos x < \dfrac{1}{\sqrt{x^2 + 1}}$$$
Lean4
theorem cos_lt_one_div_sqrt_sq_add_one {x : ℝ} (hx1 : -(3 * π / 2) ≤ x) (hx2 : x ≤ 3 * π / 2) (hx3 : x ≠ 0) :
cos x < (1 / √(x ^ 2 + 1) : ℝ) :=
by
suffices ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
by
rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
· exact this h hx2
· convert this (by linarith : 0 < -x) (by linarith) using 1
· rw [cos_neg]
· rw [neg_sq]
intro y hy1 hy2
have hy3 : ↑0 < y ^ 2 + 1 := by linarith [sq_nonneg y]
rcases lt_or_ge y (π / 2) with (hy2' | hy1')
· -- Main case : `0 < y < π / 2`
have hy4 : 0 < cos y := cos_pos_of_mem_Ioo ⟨by linarith, hy2'⟩
rw [← abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨by linarith, hy2'.le⟩), ←
abs_of_nonneg (one_div_nonneg.mpr (sqrt_nonneg _)), ← sq_lt_sq, div_pow, one_pow, sq_sqrt hy3.le,
lt_one_div (pow_pos hy4 _) hy3, ← inv_one_add_tan_sq hy4.ne', one_div, inv_inv, add_comm, add_lt_add_iff_left,
sq_lt_sq, abs_of_pos hy1, abs_of_nonneg (tan_nonneg_of_nonneg_of_le_pi_div_two hy1.le hy2'.le)]
exact Real.lt_tan hy1 hy2'
· -- Easy case : `π / 2 ≤ y ≤ 3 * π / 2`
refine lt_of_le_of_lt ?_ (one_div_pos.mpr <| sqrt_pos_of_pos hy3)
exact cos_nonpos_of_pi_div_two_le_of_le hy1' (by linarith [pi_pos])
