Analysis I, Section 10.1: Basic definitions

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• API for Mathlib's HasDerivWithinAt, derivWithin, and DifferentiableWithinAt.

Note that the Mathlib conventions differ slightly from that in the text, in that differentiability is defined even at points that are not limit points of the domain; derivatives in such cases may not be unique, but derivWithin still selects one such derivative in such cases (or 0, if no derivative exists).

theorem HasDerivWithinAt.iff (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) (L : ℝ) : HasDerivWithinAt f L X x₀ ↔ Filter.Tendsto (fun (x : ℝ) => (f x - f x₀) / (x - x₀)) (nhdsWithin x₀ (X \ {x₀})) (nhds L)

Definition 10.1.1 (Differentiability at a point). For the Mathlib notion HasDerivWithinAt, the hypothesis that x₀ is a limit point is not needed.

theorem DifferentiableWithinAt.iff (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) : DifferentiableWithinAt ℝ f X x₀ ↔ ∃ (L : ℝ), HasDerivWithinAt f L X x₀

theorem DifferentiableWithinAt.of_hasDeriv {X : Set ℝ} {x₀ : ℝ} {f : ℝ → ℝ} {L : ℝ} (hL : HasDerivWithinAt f L X x₀) : DifferentiableWithinAt ℝ f X x₀

theorem Chapter10.derivative_unique {X : Set ℝ} {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} {L L' : ℝ} (hL : HasDerivWithinAt f L X x₀) (hL' : HasDerivWithinAt f L' X x₀) : L = L'

theorem Chapter10.derivative_unique' (X : Set ℝ) {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} {L : ℝ} (hL : HasDerivWithinAt f L X x₀) (hdiff : DifferentiableWithinAt ℝ f X x₀) : L = derivWithin f X x₀

@[reducible, inline]

abbrev Chapter10.f_10_1_6 : ℝ → ℝ

Example 10.1.6

Equations

• Chapter10.f_10_1_6 = abs

theorem HasDerivWithinAt.iff_approx_linear (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) (L : ℝ) : HasDerivWithinAt f L X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀ - L * (x - x₀)| ≤ ε * |x - x₀|

Proposition 10.1.7 (Newton's approximation) / Exercise 10.1.2

theorem ContinuousWithinAt.of_differentiableWithinAt {X : Set ℝ} {x₀ : ℝ} {f : ℝ → ℝ} (h : DifferentiableWithinAt ℝ f X x₀) : ContinuousWithinAt f X x₀

Proposition 10.1.10 / Exercise 10.1.3

theorem ContinuousOn.of_differentiableOn {X : Set ℝ} {f : ℝ → ℝ} (h : DifferentiableOn ℝ f X) : ContinuousOn f X

Corollary 10.1.12

theorem HasDerivWithinAt.of_const (X : Set ℝ) (x₀ c : ℝ) : HasDerivWithinAt (fun (x : ℝ) => c) 0 X x₀

Theorem 10.1.13 (a) (Differential calculus) / Exercise 10.1.4

theorem HasDerivWithinAt.of_id (X : Set ℝ) (x₀ : ℝ) : HasDerivWithinAt (fun (x : ℝ) => x) 1 X x₀

Theorem 10.1.13 (b) (Differential calculus) / Exercise 10.1.4

theorem HasDerivWithinAt.of_add {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f + g) (f'x₀ + g'x₀) X x₀

Theorem 10.1.13 (c) (Sum rule) / Exercise 10.1.4

theorem HasDerivWithinAt.of_mul {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f * g) (f'x₀ * g x₀ + f x₀ * g'x₀) X x₀

Theorem 10.1.13 (d) (Product rule) / Exercise 10.1.4

theorem HasDerivWithinAt.of_smul {X : Set ℝ} {x₀ f'x₀ : ℝ} (c : ℝ) {f : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) : HasDerivWithinAt (c • f) (c * f'x₀) X x₀

Theorem 10.1.13 (e) (Differential calculus) / Exercise 10.1.4

theorem HasDerivWithinAt.of_sub {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f - g) (f'x₀ - g'x₀) X x₀

Theorem 10.1.13 (f) (Difference rule) / Exercise 10.1.4

theorem HasDerivWithinAt.of_inv {X : Set ℝ} {x₀ g'x₀ : ℝ} {g : ℝ → ℝ} (hgx₀ : g x₀ ≠ 0) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (1 / g) (-g'x₀ / g x₀ ^ 2) X x₀

Theorem 10.1.13 (g) (Differential calculus) / Exercise 10.1.4

theorem HasDerivWithinAt.of_div {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hgx₀ : g x₀ ≠ 0) (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f / g) ((f'x₀ * g x₀ - f x₀ * g'x₀) / g x₀ ^ 2) X x₀

Theorem 10.1.13 (h) (Quotient rule) / Exercise 10.1.4

theorem HasDerivWithinAt.of_comp {X Y : Set ℝ} {x₀ y₀ f'x₀ g'y₀ : ℝ} {f g : ℝ → ℝ} (hfx₀ : f x₀ = y₀) (hfX : ∀ x ∈ X, f x ∈ Y) (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'y₀ Y y₀) : HasDerivWithinAt (g ∘ f) (g'y₀ * f'x₀) X x₀

Theorem 10.1.15 (Chain rule) / Exercise 10.1.7

theorem HasDerivWithinAt.of_pow (n : ℕ) (x₀ : ℝ) : HasDerivWithinAt (fun (x : ℝ) => x ^ n) (↑n * x₀ ^ (↑n - 1)) Set.univ x₀

Exercise 10.1.5

theorem HasDerivWithinAt.of_zpow (n : ℤ) (x₀ : ℝ) (hx₀ : x₀ ≠ 0) : HasDerivWithinAt (fun (x : ℝ) => x ^ n) (↑n * x₀ ^ (n - 1)) (Set.univ \ {0}) x₀

Exercise 10.1.6