Documentation

Analysis.Section_10_1

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

source
theorem DifferentiableWithinAt.iff (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) :
DifferentiableWithinAt ℝ f X x₀ ↔ ∃ (L : ℝ), HasDerivWithinAt f L X x₀
source
theorem DifferentiableWithinAt.of_hasDeriv {X : Set ℝ} {x₀ : ℝ} {f : ℝ → ℝ} {L : ℝ} (hL : HasDerivWithinAt f L X x₀) :
DifferentiableWithinAt ℝ f X x₀
source
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'
source
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₀
source
@[reducible, inline]
abbrev Chapter10.f_10_1_6 :
ℝ → ℝ

Example 10.1.6

Equations
Instances For
    source
    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

    source
    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

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

    Corollary 10.1.12

    source
    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

    source
    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

    source
    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

    source
    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

    source
    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

    source
    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

    source
    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

    source
    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

    source
    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

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

    Exercise 10.1.5

    source
    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