Real.hasDerivAt_tan
theorem Real.hasDerivAt_tan : ∀ {x : ℝ}, x.cos ≠ 0 → HasDerivAt Real.tan (1 / x.cos ^ 2) x
The theorem `Real.hasDerivAt_tan` states that for every real number `x`, if the cosine of `x` is not equal to 0, then the tangent function has a derivative at `x`, and the value of the derivative is `1 / (cos(x))^2`. In mathematical terms, this is demonstrating that wherever the cosine function doesn't equal zero, the derivative of the tangent function is equal to the secant squared function.
More concisely: For every real number `x` with `cos(x) ≠ 0`, the derivative of the tangent function at `x` is equal to `1 / (cos(x))^2`.
|
Real.hasStrictDerivAt_arctan
theorem Real.hasStrictDerivAt_arctan : ∀ (x : ℝ), HasStrictDerivAt Real.arctan (1 / (1 + x ^ 2)) x
This theorem states that for every real number `x`, the function `arctan` (which is the inverse of the tangent function) has a strict derivative at the point `x`. The value of this derivative is `1 / (1 + x ^ 2)`. In other words, the derivative of the `arctan` function at any point `x` is calculated as the reciprocal of the sum of 1 and the square of `x`. This is a strict derivative, which means the function is smooth or continuously differentiable at that point.
More concisely: The derivative of the real function `arctan` is `1 / (1 + x^2)` for all real `x`.
|
Real.hasDerivAt_arctan'
theorem Real.hasDerivAt_arctan' : ∀ (x : ℝ), HasDerivAt Real.arctan (1 + x ^ 2)⁻¹ x
The theorem `Real.hasDerivAt_arctan'` states that for every real number `x`, the function `Real.arctan` has a derivative at the point `x`. The derivative of the function at `x` is given by `(1 + x ^ 2)⁻¹`. In mathematical terms, this is expressing that the derivative of the arctan function at any point x is 1/(1 + x²).
More concisely: The theorem `Real.hasDerivAt_arctan` asserts that the derivative of the arctan function is 1/(1 + x²) for every real number x.
|
Real.hasDerivAt_arctan
theorem Real.hasDerivAt_arctan : ∀ (x : ℝ), HasDerivAt Real.arctan (1 / (1 + x ^ 2)) x
This theorem states that for all real numbers `x`, the derivative of the arctan function at the point `x` is `1 / (1 + x ^ 2)`. In other words, if you were to draw a tangent line at any point on the graph of the arctan function, the slope of that line would be `1 / (1 + x ^ 2)`. This is a fundamental result in calculus and is used extensively in areas of mathematics that involve trigonometry and differentiation.
More concisely: The derivative of the arctan function is equal to 1 / (1 + x^2).
|
Real.contDiff_arctan
theorem Real.contDiff_arctan : ∀ {n : ℕ∞}, ContDiff ℝ n Real.arctan
The theorem `Real.contDiff_arctan` states that the function `Real.arctan`, which is the inverse of the tangent function and returns values in the range `-π / 2 < arctan x` and `arctan x < π / 2`, is continuously differentiable for all natural numbers `n`, including infinity. In other words, the arctan function has derivatives of all orders and these derivatives are continuous functions.
More concisely: The arctan function, defined on the real numbers, is continuously differentiable for all natural numbers, including infinity.
|