Analysis
10.1. Basic definitions

Imports

import Mathlib.Tactic
import Mathlib.Analysis.Calculus.Deriv.Basic

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).

namespace Chapter10variable (x₀ : ℝ)

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 _root_.HasDerivWithinAt.iff (X: Set ℝ) (x₀ : ℝ) (f: ℝ → ℝ)
  (L:ℝ) :
  HasDerivWithinAt f L X x₀ ↔ (nhdsWithin x₀ (X \ {x₀})).Tendsto (fun x ↦ (f x - f x₀) / (x - x₀))
   (nhds L) :=  byX: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)
  rw [hasDerivWithinAt_iff_tendsto_slope, iff_iff_eq, slope_fun_def_field]All goals completed! 🐙

theorem _root_.DifferentiableWithinAt.iff (X: Set ℝ) (x₀ : ℝ) (f: ℝ → ℝ) :
  DifferentiableWithinAt ℝ f X x₀ ↔ ∃ L, HasDerivWithinAt f L X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝ⊢ DifferentiableWithinAt ℝ f X x₀ ↔ ∃ L, HasDerivWithinAt f L X x₀
  constructormpX:Set ℝx₀:ℝf:ℝ → ℝ⊢ DifferentiableWithinAt ℝ f X x₀ → ∃ L, HasDerivWithinAt f L X x₀mprX:Set ℝx₀:ℝf:ℝ → ℝ⊢ (∃ L, HasDerivWithinAt f L X x₀) → DifferentiableWithinAt ℝ f X x₀
  .mpX:Set ℝx₀:ℝf:ℝ → ℝ⊢ DifferentiableWithinAt ℝ f X x₀ → ∃ L, HasDerivWithinAt f L X x₀ intro hmpX:Set ℝx₀:ℝf:ℝ → ℝh:DifferentiableWithinAt ℝ f X x₀⊢ ∃ L, HasDerivWithinAt f L X x₀; use derivWithin f X x₀hX:Set ℝx₀:ℝf:ℝ → ℝh:DifferentiableWithinAt ℝ f X x₀⊢ HasDerivWithinAt f (derivWithin f X x₀) X x₀; exact h.hasDerivWithinAtAll goals completed! 🐙
  intro ⟨ L, h ⟩mprX:Set ℝx₀:ℝf:ℝ → ℝL:ℝh:HasDerivWithinAt f L X x₀⊢ DifferentiableWithinAt ℝ f X x₀; exact h.differentiableWithinAtAll goals completed! 🐙

theorem _root_.DifferentiableWithinAt.of_hasDeriv {X: Set ℝ} {x₀ : ℝ} {f: ℝ → ℝ} {L:ℝ}
  (hL: HasDerivWithinAt f L X x₀) : DifferentiableWithinAt ℝ f X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝL:ℝhL:HasDerivWithinAt f L X x₀⊢ DifferentiableWithinAt ℝ f X x₀
  rw [DifferentiableWithinAt.iff]X:Set ℝx₀:ℝf:ℝ → ℝL:ℝhL:HasDerivWithinAt f L X x₀⊢ ∃ L, HasDerivWithinAt f L X x₀; use LAll goals completed! 🐙

theorem derivative_unique {X: Set ℝ} {x₀ : ℝ}
  (hx₀: ClusterPt x₀ (.principal (X \ {x₀}))) {f: ℝ → ℝ} {L L':ℝ}
  (hL: HasDerivWithinAt f L X x₀) (hL': HasDerivWithinAt f L' X x₀) :
  L = L' := byX: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'
    rw [_root_.HasDerivWithinAt.iff] at hL hL'X:Set ℝx₀:ℝhx₀:ClusterPt x₀ (Filter.principal (X \ {x₀}))f:ℝ → ℝL:ℝL':ℝhL:Filter.Tendsto (fun x ↦ (f x - f x₀) / (x - x₀)) (nhdsWithin x₀ (X \ {x₀})) (nhds L)hL':Filter.Tendsto (fun x ↦ (f x - f x₀) / (x - x₀)) (nhdsWithin x₀ (X \ {x₀})) (nhds L')⊢ L = L'
    rw [ClusterPt.eq_1] at hx₀X:Set ℝx₀:ℝhx₀:(nhds x₀ ⊓ Filter.principal (X \ {x₀})).NeBotf:ℝ → ℝL:ℝL':ℝhL:Filter.Tendsto (fun x ↦ (f x - f x₀) / (x - x₀)) (nhdsWithin x₀ (X \ {x₀})) (nhds L)hL':Filter.Tendsto (fun x ↦ (f x - f x₀) / (x - x₀)) (nhdsWithin x₀ (X \ {x₀})) (nhds L')⊢ L = L'
    solve_by_elim [tendsto_nhds_unique]All goals completed! 🐙

DifferentiableWithinAt.hasDerivWithinAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 f s x) :
  HasDerivWithinAt f (derivWithin f s x) s x#check DifferentiableWithinAt.hasDerivWithinAt

DifferentiableWithinAt.hasDerivWithinAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 f s x) :
  HasDerivWithinAt f (derivWithin f s x) s x

theorem derivative_unique' (X: Set ℝ) {x₀ : ℝ}
  (hx₀: ClusterPt x₀ (.principal (X \ {x₀}))) {f: ℝ → ℝ} {L :ℝ}
  (hL: HasDerivWithinAt f L X x₀)
  (hdiff : DifferentiableWithinAt ℝ f X x₀):
  L = derivWithin f X x₀ := byX: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₀
  solve_by_elim [derivative_unique, DifferentiableWithinAt.hasDerivWithinAt]All goals completed! 🐙

/-- Example 10.1.3 -/
declaration uses `sorry`example (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^2) (2 * x₀) .univ x₀ := byx₀✝:ℝx₀:ℝ⊢ HasDerivWithinAt (fun x ↦ x ^ 2) (2 * x₀) Set.univ x₀
  sorryAll goals completed! 🐙

declaration uses `sorry`example (x₀:ℝ) : DifferentiableWithinAt ℝ (fun x ↦ x^2) .univ x₀ := byx₀✝:ℝx₀:ℝ⊢ DifferentiableWithinAt ℝ (fun x ↦ x ^ 2) Set.univ x₀
  sorryAll goals completed! 🐙

declaration uses `sorry`example (x₀:ℝ) : derivWithin (fun x ↦ x^2) .univ x₀ = 2 * x₀ := byx₀✝:ℝx₀:ℝ⊢ derivWithin (fun x ↦ x ^ 2) Set.univ x₀ = 2 * x₀
  sorryAll goals completed! 🐙

/-- Remark 10.1.4 -/
example (X: Set ℝ) (x₀ : ℝ) {f g: ℝ → ℝ} (hfg: f = g):
  DifferentiableWithinAt ℝ f X x₀ ↔ DifferentiableWithinAt ℝ g X x₀ := byx₀✝:ℝX:Set ℝx₀:ℝf:ℝ → ℝg:ℝ → ℝhfg:f = g⊢ DifferentiableWithinAt ℝ f X x₀ ↔ DifferentiableWithinAt ℝ g X x₀ rw [hfg]All goals completed! 🐙

example (X: Set ℝ) (x₀ : ℝ) {f g: ℝ → ℝ} (L:ℝ) (hfg: f = g):
  HasDerivWithinAt f L X x₀ ↔ HasDerivWithinAt g L X x₀ := byx₀✝:ℝX:Set ℝx₀:ℝf:ℝ → ℝg:ℝ → ℝL:ℝhfg:f = g⊢ HasDerivWithinAt f L X x₀ ↔ HasDerivWithinAt g L X x₀ rw [hfg]All goals completed! 🐙

declaration uses `sorry`example : ∃ (X: Set ℝ) (x₀ :ℝ) (f g: ℝ → ℝ) (L:ℝ) (hfg: f x₀ = g x₀),
  HasDerivWithinAt f L X x₀ ∧ ¬ HasDerivWithinAt g L X x₀ := byx₀:ℝ⊢ ∃ X x₀ f g L, ∃ (_ : f x₀ = g x₀), HasDerivWithinAt f L X x₀ ∧ ¬HasDerivWithinAt g L X x₀
  sorryAll goals completed! 🐙

Example 10.1.6

abbrev f_10_1_6 : ℝ → ℝ := abs

              declaration uses `sorry`example : (nhdsWithin 0 (.Ioi 0)).Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds 1) := byx₀:ℝ⊢ Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
  sorryAll goals completed! 🐙declaration uses `sorry`example : (nhdsWithin 0 (.Iio 0)).Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds (-1)) := byx₀:ℝ⊢ Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhdsWithin 0 (Set.Iio 0)) (nhds (-1))
  sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ ∃ L, (nhdsWithin 0 (.univ \ {0})).Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
   (nhds L) := byx₀:ℝ⊢ ¬∃ L, Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhdsWithin 0 (Set.univ \ {0})) (nhds L) sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ DifferentiableWithinAt ℝ f_10_1_6 (.univ) 0 := byx₀:ℝ⊢ ¬DifferentiableWithinAt ℝ f_10_1_6 Set.univ 0
  sorryAll goals completed! 🐙declaration uses `sorry`example : DifferentiableWithinAt ℝ f_10_1_6 (.Ioi 0) 0 := byx₀:ℝ⊢ DifferentiableWithinAt ℝ f_10_1_6 (Set.Ioi 0) 0
  sorryAll goals completed! 🐙declaration uses `sorry`example : derivWithin f_10_1_6 (.Ioi 0) 0 = 1 := byx₀:ℝ⊢ derivWithin f_10_1_6 (Set.Ioi 0) 0 = 1
  sorryAll goals completed! 🐙declaration uses `sorry`example : DifferentiableWithinAt ℝ f_10_1_6 (.Iio 0) 0 := byx₀:ℝ⊢ DifferentiableWithinAt ℝ f_10_1_6 (Set.Iio 0) 0
  sorryAll goals completed! 🐙declaration uses `sorry`example : derivWithin f_10_1_6 (.Iio 0) 0 = -1 := byx₀:ℝ⊢ derivWithin f_10_1_6 (Set.Iio 0) 0 = -1
  sorryAll goals completed! 🐙

Proposition 10.1.7 (Newton's approximation) / Exercise 10.1.2

theorem declaration uses `sorry`_root_.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₀| := byX:Set ℝx₀:ℝf:ℝ → ℝL:ℝ⊢ HasDerivWithinAt f L X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀ - L * (x - x₀)| ≤ ε * |x - x₀|
  sorryAll goals completed! 🐙

Proposition 10.1.10 / Exercise 10.1.3

theorem declaration uses `sorry`_root_.ContinuousWithinAt.of_differentiableWithinAt {X: Set ℝ} {x₀ : ℝ} {f: ℝ → ℝ}
  (h: DifferentiableWithinAt ℝ f X x₀) :
  ContinuousWithinAt f X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝh:DifferentiableWithinAt ℝ f X x₀⊢ ContinuousWithinAt f X x₀
  sorryAll goals completed! 🐙

/-Definition 10.1.11 (Differentiability on a domain)-/
DifferentiableOn.eq_1.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E]
  [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F)
  (s : Set E) : DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x#check DifferentiableOn.eq_1

Corollary 10.1.12

theorem _root_.ContinuousOn.of_differentiableOn {X: Set ℝ} {f: ℝ → ℝ}
  (h: DifferentiableOn ℝ f X) :
  ContinuousOn f X := byX:Set ℝf:ℝ → ℝh:DifferentiableOn ℝ f X⊢ ContinuousOn f X
  solve_by_elim [ContinuousWithinAt.of_differentiableWithinAt]All goals completed! 🐙

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

theorem declaration uses `sorry`_root_.HasDerivWithinAt.of_const (X: Set ℝ) (x₀ : ℝ) (c:ℝ) :
  HasDerivWithinAt (fun x ↦ c) 0 X x₀ := byX:Set ℝx₀:ℝc:ℝ⊢ HasDerivWithinAt (fun x ↦ c) 0 X x₀ sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.HasDerivWithinAt.of_id (X: Set ℝ) (x₀ : ℝ) :
  HasDerivWithinAt (fun x ↦ x) 1 X x₀ := byX:Set ℝx₀:ℝ⊢ HasDerivWithinAt (fun x ↦ x) 1 X x₀ sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.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₀ := byX: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₀
  sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.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₀ := byX: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₀
  sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.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₀ := byX:Set ℝx₀:ℝf'x₀:ℝc:ℝf:ℝ → ℝhf:HasDerivWithinAt f f'x₀ X x₀⊢ HasDerivWithinAt (c • f) (c * f'x₀) X x₀
  sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.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₀ := byX: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₀
  sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.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₀ := byX:Set ℝx₀:ℝg'x₀:ℝg:ℝ → ℝhgx₀:g x₀ ≠ 0hg:HasDerivWithinAt g g'x₀ X x₀⊢ HasDerivWithinAt (1 / g) (-g'x₀ / g x₀ ^ 2) X x₀
  sorryAll goals completed! 🐙

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

theorem declaration uses `sorry`_root_.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₀ := byX:Set ℝx₀:ℝf'x₀:ℝg'x₀:ℝf:ℝ → ℝg:ℝ → ℝhgx₀:g x₀ ≠ 0hf: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₀
  sorryAll goals completed! 🐙

declaration uses `sorry`example (x₀:ℝ) (hx₀: x₀ ≠ 1): HasDerivWithinAt (fun x ↦ (x-2)/(x-1)) (1 /(x₀-1)^2) (.univ \ {1}) x₀ := byx₀✝:ℝx₀:ℝhx₀:x₀ ≠ 1⊢ HasDerivWithinAt (fun x ↦ (x - 2) / (x - 1)) (1 / (x₀ - 1) ^ 2) (Set.univ \ {1}) x₀
  sorryAll goals completed! 🐙

Theorem 10.1.15 (Chain rule) / Exercise 10.1.7

theorem declaration uses `sorry`_root_.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₀ := byX:Set ℝY:Set ℝx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝf:ℝ → ℝg:ℝ → ℝhfx₀:f x₀ = y₀hfX:∀ x ∈ X, f x ∈ Yhf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ HasDerivWithinAt (g ∘ f) (g'y₀ * f'x₀) X x₀
  sorryAll goals completed! 🐙

Exercise 10.1.5

theorem declaration uses `sorry`_root_.HasDerivWithinAt.of_pow (n:ℕ) (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^n)
(n * x₀^((n:ℤ)-1)) .univ x₀ := byn:ℕx₀:ℝ⊢ HasDerivWithinAt (fun x ↦ x ^ n) (↑n * x₀ ^ (↑n - 1)) Set.univ x₀
  sorryAll goals completed! 🐙

Exercise 10.1.6

theorem declaration uses `sorry`_root_.HasDerivWithinAt.of_zpow (n:ℤ) (x₀:ℝ) (hx₀: x₀ ≠ 0) :
  HasDerivWithinAt (fun x ↦ x^n) (n * x₀^(n-1)) (.univ \ {0}) x₀ := byn:ℤx₀:ℝhx₀:x₀ ≠ 0⊢ HasDerivWithinAt (fun x ↦ x ^ n) (↑n * x₀ ^ (n - 1)) (Set.univ \ {0}) x₀
  sorryAll goals completed! 🐙

end Chapter10