Real.sin_gt_sub_cube
theorem Real.sin_gt_sub_cube : ∀ {x : ℝ}, 0 < x → x ≤ 1 → x - x ^ 3 / 4 < x.sin
This theorem states that for any real number `x` falling between 0 and 1 (exclusive of 0 and inclusive of 1), the value of `x` subtracted by the cube of `x` divided by 4 is less than the sine of `x`. While this inequality also holds for `x` greater than 1, the proof is more complex especially for numbers just above 1. There is a tighter inequality where sine of `x` is greater than `x` subtracted by the cube of `x` divided by 6 for all `x` greater than 0, but the proof of this current inequality is simpler.
More concisely: For any real number `x` in the open interval (0, 1), the value of `x - x^3 / 4` is strictly less than the sine of `x`.
|
Real.lt_tan
theorem Real.lt_tan : ∀ {x : ℝ}, 0 < x → x < Real.pi / 2 → x < x.tan
The theorem `Real.lt_tan` states that for any real number `x` that is greater than 0 and less than pi/2 (π/2), the value of `x` is less than the tangent of `x`. This theorem is proven by showing that the function `tan x - x` equals zero at `x = 0` and its derivative is non-negative, implying that `tan x - x` is non-decreasing on the interval `(0, π/2)`, and hence `x < tan x` for `0 < x < π/2`.
More concisely: For any real number `x` in the open interval `(0, π/2)`, `x` is strictly less than its tangent value, i.e., `x < tan x`.
|
Real.deriv_tan_sub_id
theorem Real.deriv_tan_sub_id : ∀ (x : ℝ), x.cos ≠ 0 → deriv (fun y => y.tan - y) x = 1 / x.cos ^ 2 - 1
The theorem `Real.deriv_tan_sub_id` states that for any real number `x`, assuming `cos x` is not equal to zero, the derivative of the function `tan x - x` at the point `x` is equal to `1/(cos x)^2 - 1`. In mathematical terms, this means that if `f(x) = tan(x) - x` and `cos(x) ≠ 0`, then `f'(x) = 1/(cos(x))^2 - 1`.
More concisely: For real numbers `x` with `cos x ≠ 0`, the derivative of `tan x - x` at `x` is equal to `1 / (cos x)² - 1`.
|
Real.sin_lt
theorem Real.sin_lt : ∀ {x : ℝ}, 0 < x → x.sin < x
This theorem states that for any real number `x` which is greater than zero, the sine of `x` (denoted as `sin x`) is less than `x` itself. In mathematical terms, for all `x` such that `0 < x`, we have that `sin(x) < x`.
More concisely: For all real numbers `x` greater than zero, `sin x` is strictly less than `x`.
|