12. Differential Calculus
We now consider the formalization of notions from analysis, starting with differentiation in this chapter and turning integration and measure theory in the next. In Section 12.1, we stick with the setting of functions from the real numbers to the real numbers, which is familiar from any introductory calculus class. In Section 12.2, we then consider the notion of a derivative in a much broader setting.
12.1. Elementary Differential Calculus
Let f be a function from the reals to the reals.
Derivative of f at a single point:
open Real
/-- The sin function has derivative 1 at 0. -/
example : HasDerivAt sin 1 0 := by simpa using hasDerivAt_sin 0
example (x : ℝ) : DifferentiableAt ℝ sin x :=
(hasDerivAt_sin x).differentiableAt
deriv f : ℝ → ℝ: Derivative of a function f : ℝ → ℝ, and is defined to take the value 0 at any point where f is not differentiable.
example {f : ℝ → ℝ} {x a : ℝ} (h : HasDerivAt f a x) : deriv f x = a :=
h.deriv
example {f : ℝ → ℝ} {x : ℝ} (h : ¬DifferentiableAt ℝ f x) : deriv f x = 0 :=
deriv_zero_of_not_differentiableAt h