noncomputable def differenceQuotient (f : ℝ → ℝ) (c x : ℝ) : ℝ

Definition 4.1.1: For an interval I ⊆ ℝ, a function f : ℝ → ℝ, and c ∈ I, if the limit L = lim_{x → c} (f x - f c) / (x - c) exists, then f is differentiable at c, L is the derivative f' c, and the quotient (f x - f c) / (x - c) is the difference quotient. If the limit exists at every c ∈ I, then f is differentiable on I and yields a derivative function f' : I → ℝ.

Equations

• differenceQuotient f c x = (f x - f c) / (x - c)

def DifferentiableAtOn (I : Set ℝ) (f : ℝ → ℝ) (c : ℝ) : Prop

The book's notion of differentiability on a subset of ℝ via the limit of the difference quotient.

Equations

• DifferentiableAtOn I f c = (c ∈ I ∧ ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => differenceQuotient f c x) (nhdsWithin c {x : ℝ | x ≠ c}) (nhds L))

noncomputable def derivativeAtOn (I : Set ℝ) (f : ℝ → ℝ) (c : ℝ) (h : DifferentiableAtOn I f c) : ℝ

The derivative value provided by the existence of the difference-quotient limit.

Equations

• derivativeAtOn I f c h = Classical.choose ⋯

theorem differentiableAtOn_iff_hasDerivAt {I : Set ℝ} {f : ℝ → ℝ} {c : ℝ} : DifferentiableAtOn I f c ↔ c ∈ I ∧ ∃ (L : ℝ), HasDerivAt f L c

The book's differentiability notion agrees with mathlib's HasDerivAt formulation.

noncomputable def derivativeOn (I : Set ℝ) (f : ℝ → ℝ) (h : ∀ c ∈ I, DifferentiableAtOn I f c) : ↑I → ℝ

If a function is differentiable at every point of an interval, the derivative defines a function I → ℝ.

Equations

• derivativeOn I f h x = derivativeAtOn I f ↑x ⋯

theorem hasDerivAt_sq (c : ℝ) : HasDerivAt (fun (x : ℝ) => x ^ 2) (2 * c) c

Example 4.1.2: For f x = x^2 on ℝ, the derivative at any c satisfies f' c = 2c, since the difference quotient simplifies to x + c and its limit as x → c is 2c.

theorem hasDerivAt_affine (a b c : ℝ) : HasDerivAt (fun (x : ℝ) => a * x + b) a c

Example 4.1.3: For an affine function f x = a * x + b with real coefficients, the difference quotient simplifies to a, so the derivative at any point c is the constant slope a.

theorem hasDerivAt_sqrt_pos {c : ℝ} (hc : 0 < c) : HasDerivAt Real.sqrt (1 / (2 * √c)) c

Example 4.1.4: The square-root function f x = √x is differentiable for x > 0, and for each c > 0 its derivative is 1 / (2√c).

theorem differenceQuotient_abs_pos {x : ℝ} (hx : 0 < x) : differenceQuotient (fun (x : ℝ) => |x|) 0 x = 1

Example 4.1.5: The absolute-value function is not differentiable at the origin, since the difference quotient is 1 for x > 0 and -1 for x < 0.

theorem differenceQuotient_abs_neg {x : ℝ} (hx : x < 0) : differenceQuotient (fun (x : ℝ) => |x|) 0 x = -1

theorem abs_not_differentiable_at_zero : ¬DifferentiableAt ℝ (fun (x : ℝ) => |x|) 0

theorem differentiableAt_real_continuousAt {f : ℝ → ℝ} {c : ℝ} (h : DifferentiableAt ℝ f c) : ContinuousAt f c

Proposition 4.1.6: If a real function is differentiable at a point of an interval, then it is continuous at that point.

theorem deriv_const_mul_at {f : ℝ → ℝ} {c α : ℝ} (hf : DifferentiableAt ℝ f c) : DifferentiableAt ℝ (fun (x : ℝ) => α * f x) c ∧ deriv (fun (x : ℝ) => α * f x) c = α * deriv f c

Proposition 4.1.7 (Linearity): Let I be an interval and let f g : ℝ → ℝ be differentiable at c ∈ I, with α : ℝ. (i) For h x = α * f x, the derivative satisfies deriv h c = α * deriv f c. (ii) For h x = f x + g x, the derivative satisfies deriv h c = deriv f c + deriv g c.

theorem deriv_add_at {f g : ℝ → ℝ} {c : ℝ} (hf : DifferentiableAt ℝ f c) (hg : DifferentiableAt ℝ g c) : DifferentiableAt ℝ (fun (x : ℝ) => f x + g x) c ∧ deriv (fun (x : ℝ) => f x + g x) c = deriv f c + deriv g c

theorem deriv_mul_at {I : Set ℝ} {f g : ℝ → ℝ} {c : ℝ} (_hc : c ∈ I) (hf : DifferentiableAt ℝ f c) (hg : DifferentiableAt ℝ g c) : DifferentiableAt ℝ (fun (x : ℝ) => f x * g x) c ∧ deriv (fun (x : ℝ) => f x * g x) c = f c * deriv g c + deriv f c * g c

Proposition 4.1.8 (Product rule): For an interval I and functions f g : ℝ → ℝ differentiable at c ∈ I, the product h x = f x * g x is differentiable at c, and its derivative satisfies deriv h c = f c * deriv g c + deriv f c * g c.

theorem deriv_div_at {I : Set ℝ} {f g : ℝ → ℝ} {c : ℝ} (hc : c ∈ I) (hf : DifferentiableAt ℝ f c) (hg : DifferentiableAt ℝ g c) (hgnz : ∀ x ∈ I, g x ≠ 0) : DifferentiableAt ℝ (fun (x : ℝ) => f x / g x) c ∧ deriv (fun (x : ℝ) => f x / g x) c = (deriv f c * g c - f c * deriv g c) / g c ^ 2

Proposition 4.1.9 (Quotient rule): For an interval I and functions f g : ℝ → ℝ differentiable at c ∈ I, with g x ≠ 0 for all x ∈ I, the quotient h x = f x / g x is differentiable at c, and its derivative satisfies deriv h c = (deriv f c * g c - f c * deriv g c) / (g c)^2.

theorem hasDerivAt_comp_at {f g : ℝ → ℝ} {c : ℝ} (hgd : DifferentiableAt ℝ g c) (hfd : DifferentiableAt ℝ f (g c)) : HasDerivAt (fun (x : ℝ) => f (g x)) (deriv f (g c) * deriv g c) c

Helper lemma for Proposition 4.1.10: differentiability of the composition arises from the chain rule for HasDerivAt.

theorem deriv_comp_at {f g : ℝ → ℝ} {c : ℝ} (hgd : DifferentiableAt ℝ g c) (hfd : DifferentiableAt ℝ f (g c)) : DifferentiableAt ℝ (fun (x : ℝ) => f (g x)) c ∧ deriv (fun (x : ℝ) => f (g x)) c = deriv f (g c) * deriv g c

Proposition 4.1.10 (Chain rule): Let I₁, I₂ be intervals, with g : ℝ → ℝ differentiable at c ∈ I₁ and taking values in I₂, and f : ℝ → ℝ differentiable at g c. If h x = f (g x), then h is differentiable at c with derivative deriv f (g c) * deriv g c.