Documentation

Mathlib.Analysis.Calculus.IteratedDeriv.Defs

One-dimensional iterated derivatives #

We define the n-th derivative of a function f : π•œ β†’ F as a function iteratedDeriv n f : π•œ β†’ F, as well as a version on domains iteratedDerivWithin n f s : π•œ β†’ F, and prove their basic properties.

Main definitions and results #

Let π•œ be a nontrivially normed field, and F a normed vector space over π•œ. Let f : π•œ β†’ F.

Implementation details #

The results are deduced from the corresponding results for the more general (multilinear) iterated FrΓ©chet derivative. For this, we write iteratedDeriv n f as the composition of iteratedFDeriv π•œ n f and a continuous linear equiv. As continuous linear equivs respect differentiability and commute with differentiation, this makes it possible to prove readily that the derivative of the n-th derivative is the n+1-th derivative in iteratedDerivWithin_succ, by translating the corresponding result iteratedFDerivWithin_succ_apply_left for the iterated FrΓ©chet derivative.

def iteratedDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•) (f : π•œ β†’ F) (x : π•œ) :
F

The n-th iterated derivative of a function from π•œ to F, as a function from π•œ to F.

Equations
Instances For
    def iteratedDerivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•) (f : π•œ β†’ F) (s : Set π•œ) (x : π•œ) :
    F

    The n-th iterated derivative of a function from π•œ to F within a set s, as a function from π•œ to F.

    Equations
    Instances For
      theorem iteratedDerivWithin_univ {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} :

      Properties of the iterated derivative within a set #

      theorem iteratedDerivWithin_eq_iteratedFDerivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} :
      iteratedDerivWithin n f s x = (iteratedFDerivWithin π•œ n f s x) fun (x : Fin n) => 1
      theorem iteratedDerivWithin_eq_equiv_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} :

      Write the iterated derivative as the composition of a continuous linear equiv and the iterated FrΓ©chet derivative

      theorem iteratedFDerivWithin_eq_equiv_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} :

      Write the iterated FrΓ©chet derivative as the composition of a continuous linear equiv and the iterated derivative.

      theorem iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} {m : Fin n β†’ π•œ} :
      (iteratedFDerivWithin π•œ n f s x) m = (∏ i : Fin n, m i) β€’ iteratedDerivWithin n f s x

      The n-th FrΓ©chet derivative applied to a vector (m 0, ..., m (n-1)) is the derivative multiplied by the product of the m is.

      theorem norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} :
      @[simp]
      theorem iteratedDerivWithin_zero {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} :
      @[simp]
      theorem iteratedDerivWithin_one {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} (h : UniqueDiffWithinAt π•œ s x) :
      theorem contDiffOn_of_continuousOn_differentiableOn_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {n : β„•βˆž} (Hcont : βˆ€ (m : β„•), ↑m ≀ n β†’ ContinuousOn (fun (x : π•œ) => iteratedDerivWithin m f s x) s) (Hdiff : βˆ€ (m : β„•), ↑m < n β†’ DifferentiableOn π•œ (fun (x : π•œ) => iteratedDerivWithin m f s x) s) :
      ContDiffOn π•œ n f s

      If the first n derivatives within a set of a function are continuous, and its first n-1 derivatives are differentiable, then the function is C^n. This is not an equivalence in general, but this is an equivalence when the set has unique derivatives, see contDiffOn_iff_continuousOn_differentiableOn_deriv.

      theorem contDiffOn_of_differentiableOn_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {n : β„•βˆž} (h : βˆ€ (m : β„•), ↑m ≀ n β†’ DifferentiableOn π•œ (iteratedDerivWithin m f s) s) :
      ContDiffOn π•œ n f s

      To check that a function is n times continuously differentiable, it suffices to check that its first n derivatives are differentiable. This is slightly too strong as the condition we require on the n-th derivative is differentiability instead of continuity, but it has the advantage of avoiding the discussion of continuity in the proof (and for n = ∞ this is optimal).

      theorem ContDiffOn.continuousOn_iteratedDerivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {n : β„•βˆž} {m : β„•} (h : ContDiffOn π•œ n f s) (hmn : ↑m ≀ n) (hs : UniqueDiffOn π•œ s) :

      On a set with unique derivatives, a C^n function has derivatives up to n which are continuous.

      theorem ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} {n : β„•βˆž} {m : β„•} (h : ContDiffWithinAt π•œ n f s x) (hmn : ↑m < n) (hs : UniqueDiffOn π•œ (insert x s)) :
      theorem ContDiffOn.differentiableOn_iteratedDerivWithin {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {n : β„•βˆž} {m : β„•} (h : ContDiffOn π•œ n f s) (hmn : ↑m < n) (hs : UniqueDiffOn π•œ s) :

      On a set with unique derivatives, a C^n function has derivatives less than n which are differentiable.

      theorem contDiffOn_iff_continuousOn_differentiableOn_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {n : β„•βˆž} (hs : UniqueDiffOn π•œ s) :
      ContDiffOn π•œ n f s ↔ (βˆ€ (m : β„•), ↑m ≀ n β†’ ContinuousOn (iteratedDerivWithin m f s) s) ∧ βˆ€ (m : β„•), ↑m < n β†’ DifferentiableOn π•œ (iteratedDerivWithin m f s) s

      The property of being C^n, initially defined in terms of the FrΓ©chet derivative, can be reformulated in terms of the one-dimensional derivative on sets with unique derivatives.

      theorem iteratedDerivWithin_succ {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} (hxs : UniqueDiffWithinAt π•œ s x) :

      The n+1-th iterated derivative within a set with unique derivatives can be obtained by differentiating the n-th iterated derivative.

      theorem iteratedDerivWithin_eq_iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} (hs : UniqueDiffOn π•œ s) (hx : x ∈ s) :
      iteratedDerivWithin n f s x = (fun (g : π•œ β†’ F) => derivWithin g s)^[n] f x

      The n-th iterated derivative within a set with unique derivatives can be obtained by iterating n times the differentiation operation.

      theorem iteratedDerivWithin_succ' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {s : Set π•œ} {x : π•œ} (hxs : UniqueDiffOn π•œ s) (hx : x ∈ s) :

      The n+1-th iterated derivative within a set with unique derivatives can be obtained by taking the n-th derivative of the derivative.

      Properties of the iterated derivative on the whole space #

      theorem iteratedDeriv_eq_iteratedFDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {x : π•œ} :
      iteratedDeriv n f x = (iteratedFDeriv π•œ n f x) fun (x : Fin n) => 1
      theorem iteratedDeriv_eq_equiv_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} :
      iteratedDeriv n f = ⇑(ContinuousMultilinearMap.piFieldEquiv π•œ (Fin n) F).symm ∘ iteratedFDeriv π•œ n f

      Write the iterated derivative as the composition of a continuous linear equiv and the iterated FrΓ©chet derivative

      theorem iteratedFDeriv_eq_equiv_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} :

      Write the iterated FrΓ©chet derivative as the composition of a continuous linear equiv and the iterated derivative.

      theorem iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {x : π•œ} {m : Fin n β†’ π•œ} :
      (iteratedFDeriv π•œ n f x) m = (∏ i : Fin n, m i) β€’ iteratedDeriv n f x

      The n-th FrΓ©chet derivative applied to a vector (m 0, ..., m (n-1)) is the derivative multiplied by the product of the m is.

      theorem norm_iteratedFDeriv_eq_norm_iteratedDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} {x : π•œ} :
      @[simp]
      theorem iteratedDeriv_zero {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} :
      @[simp]
      theorem iteratedDeriv_one {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} :
      theorem contDiff_iff_iteratedDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {n : β„•βˆž} :
      ContDiff π•œ n f ↔ (βˆ€ (m : β„•), ↑m ≀ n β†’ Continuous (iteratedDeriv m f)) ∧ βˆ€ (m : β„•), ↑m < n β†’ Differentiable π•œ (iteratedDeriv m f)

      The property of being C^n, initially defined in terms of the FrΓ©chet derivative, can be reformulated in terms of the one-dimensional derivative.

      theorem contDiff_of_differentiable_iteratedDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {n : β„•βˆž} (h : βˆ€ (m : β„•), ↑m ≀ n β†’ Differentiable π•œ (iteratedDeriv m f)) :
      ContDiff π•œ n f

      To check that a function is n times continuously differentiable, it suffices to check that its first n derivatives are differentiable. This is slightly too strong as the condition we require on the n-th derivative is differentiability instead of continuity, but it has the advantage of avoiding the discussion of continuity in the proof (and for n = ∞ this is optimal).

      theorem ContDiff.continuous_iteratedDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {n : β„•βˆž} (m : β„•) (h : ContDiff π•œ n f) (hmn : ↑m ≀ n) :
      theorem ContDiff.differentiable_iteratedDeriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {n : β„•βˆž} (m : β„•) (h : ContDiff π•œ n f) (hmn : ↑m < n) :
      theorem iteratedDeriv_succ {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} :

      The n+1-th iterated derivative can be obtained by differentiating the n-th iterated derivative.

      theorem iteratedDeriv_eq_iterate {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} :
      iteratedDeriv n f = deriv^[n] f

      The n-th iterated derivative can be obtained by iterating n times the differentiation operation.

      theorem iteratedDeriv_succ' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•} {f : π•œ β†’ F} :

      The n+1-th iterated derivative can be obtained by taking the n-th derivative of the derivative.