Real.hasDerivAt_sqrt
theorem Real.hasDerivAt_sqrt : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt (fun x => x.sqrt) (1 / (2 * x.sqrt)) x
The theorem `Real.hasDerivAt_sqrt` states that for all real numbers `x`, if `x` is not equal to 0, then the square root function `Real.sqrt` has a derivative at the point `x` which is equal to `1 / (2 * Real.sqrt x)`. This means that the rate of change of the square root function at any non-zero point `x` is given by `1 / (2 * Real.sqrt x)`. This is a formalization of the well-known result from calculus that the derivative of the square root of `x` is `1 / (2 * sqrt(x))`, where `sqrt(x)` denotes the square root of `x`.
More concisely: For all non-zero real numbers x, the derivative of the square root function at x is 1 / (2 * √x).
|
Real.hasStrictDerivAt_sqrt
theorem Real.hasStrictDerivAt_sqrt : ∀ {x : ℝ}, x ≠ 0 → HasStrictDerivAt (fun x => x.sqrt) (1 / (2 * x.sqrt)) x := by
sorry
The theorem `Real.hasStrictDerivAt_sqrt` states that for all real numbers `x` that are not equal to zero, the function `Real.sqrt` (which computes the square root of a real number) has a strict derivative at the point `x`. The derivative of `Real.sqrt` at `x` is given by the expression `1 / (2 * Real.sqrt x)`. In mathematical notation, this can be written as: if $x \neq 0$, then $\frac{d}{dx}\sqrt{x} = \frac{1}{2\sqrt{x}}$. This means that the rate of change of the square root function at point `x` is one half the reciprocal of the square root of `x`.
More concisely: For all non-zero real numbers x, the square root function has a strict derivative equal to 1 / (2 * √x).
|
Real.contDiffAt_sqrt
theorem Real.contDiffAt_sqrt : ∀ {x : ℝ} {n : ℕ∞}, x ≠ 0 → ContDiffAt ℝ n (fun x => x.sqrt) x
This theorem states that the square root function is continuously differentiable at any non-zero real number. Here, `ContDiffAt ℝ n Real.sqrt x` means that the square root function `Real.sqrt` is n-times continuously differentiable at the point `x` in the real numbers. This property holds for any real number `x` that is not equal to zero, and for any `n` in the extended natural numbers (which includes infinity).
More concisely: The square root function `Real.sqrt` is continuously differentiable for all non-zero real numbers `x`.
|