# Fréchet derivatives of analytic functions. #

A function expressible as a power series at a point has a Fréchet derivative there. Also the special case in terms of `deriv` when the domain is 1-dimensional.

As an application, we show that continuous multilinear maps are smooth. We also compute their iterated derivatives, in `ContinuousMultilinearMap.iteratedFDeriv_eq`.

## Main definitions and results #

- `AnalyticAt.differentiableAt` : an analytic function at a point is differentiable there.
- `AnalyticOnNhd.fderiv` : in a complete space, if a function is analytic on a neighborhood of a set `s`, so is its derivative.
- `AnalyticOnNhd.fderiv_of_isOpen` : if a function is analytic on a neighborhood of an open set `s`, so is its derivative.
- `AnalyticOn.fderivWithin` : if a function is analytic on a set of unique differentiability, so is its derivative within this set.
- `OpenPartialHomeomorph.analyticAt_symm` : if an open partial homeomorphism `f` is analytic at a point `f.symm a`, with invertible derivative, then its inverse is analytic at `a`.

## Comments on completeness #

Some theorems need a complete space, some don't, for the following reason.

(1) If a function is analytic at a point `x`, then it is differentiable there (with derivative given by the first term in the power series). There is no issue of convergence here.

(2) If a function has a power series on a ball `B (x, r)`, there is no guarantee that the power series for the derivative will converge at `y ≠ x`, if the space is not complete. So, to deduce that `f` is differentiable at `y`, one needs completeness in general.

(3) However, if a function `f` has a power series on a ball `B (x, r)`, and is a priori known to be differentiable at some point `y ≠ x`, then the power series for the derivative of `f` will automatically converge at `y`, towards the given derivative: this follows from the facts that this is true in the completion (thanks to the previous point) and that the map to the completion is an embedding.

(4) Therefore, if one assumes `AnalyticOn 𝕜 f s` where `s` is an open set, then `f` is analytic therefore differentiable at every point of `s`, by (1), so by (3) the power series for its derivative converges on whole balls. Therefore, the derivative of `f` is also analytic on `s`. The same holds if `s` is merely a set with unique differentials.

(5) However, this does not work for `AnalyticOnNhd 𝕜 f s`, as we don't get for free differentiability at points in a neighborhood of `s`. Therefore, the theorem that deduces `AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s` from `AnalyticOnNhd 𝕜 f s` requires completeness of the space.

source
theorem HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E} (h : HasFPowerSeriesWithinAt f p s x) :
(fun (y : E × E) => f y.1 - f y.2 - ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (y.1 - y.2)) =o[nhdsWithin (x, x) (insert x s ×ˢ insert x s)] fun (y : E × E) => y.1 - y.2

A function which is analytic within a set is strictly differentiable there. Since we don't have a predicate `HasStrictFDerivWithinAt`, we spell out what it would mean.

source
theorem HasFPowerSeriesAt.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) :
HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
source
theorem HasFPowerSeriesWithinAt.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E} (h : HasFPowerSeriesWithinAt f p s x) :
HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (insert x s) x
source
theorem HasFPowerSeriesAt.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) :
HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
source
theorem HasFPowerSeriesWithinAt.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E} (h : HasFPowerSeriesWithinAt f p s x) :
DifferentiableWithinAt 𝕜 f (insert x s) x
source
theorem HasFPowerSeriesAt.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) :
DifferentiableAt 𝕜 f x
source
theorem AnalyticWithinAt.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : AnalyticWithinAt 𝕜 f s x) :
DifferentiableWithinAt 𝕜 f (insert x s) x
source
theorem AnalyticAt.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} :
AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x
source
theorem AnalyticAt.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : AnalyticAt 𝕜 f x) :
DifferentiableWithinAt 𝕜 f s x
source
theorem HasFPowerSeriesWithinAt.fderivWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E} (h : HasFPowerSeriesWithinAt f p s x) (hu : UniqueDiffWithinAt 𝕜 (insert x s) x) :
fderivWithin 𝕜 f (insert x s) x = (continuousMultilinearCurryFin1 𝕜 E F) (p 1)
source
theorem HasFPowerSeriesAt.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} (h : HasFPowerSeriesAt f p x) :
fderiv 𝕜 f x = (continuousMultilinearCurryFin1 𝕜 E F) (p 1)
source
theorem AnalyticAt.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
HasStrictFDerivAt f (fderiv 𝕜 f x) x
source
theorem HasFPowerSeriesWithinOnBall.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) :
DifferentiableOn 𝕜 f (insert x s ∩ EMetric.ball x r)
source
theorem HasFPowerSeriesOnBall.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) :
DifferentiableOn 𝕜 f (EMetric.ball x r)
source
theorem HasFPowerSeriesAt.eventually_differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} [CompleteSpace F] (hp : HasFPowerSeriesAt f p x) :
∀ᶠ (z : E) in nhds x, DifferentiableAt 𝕜 f z
source
theorem AnalyticOn.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) :
DifferentiableOn 𝕜 f s
source
theorem AnalyticOnNhd.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOnNhd 𝕜 f s) :
DifferentiableOn 𝕜 f s
source
theorem HasFPowerSeriesWithinOnBall.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : ↑‖y‖₊ < r) (h'y : x + y ∈ insert x s) :
HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert x s) (x + y)
source
theorem HasFPowerSeriesOnBall.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : ↑‖y‖₊ < r) :
HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
source
theorem HasFPowerSeriesWithinOnBall.fderivWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : ↑‖y‖₊ < r) (h'y : x + y ∈ insert x s) (hu : UniqueDiffOn 𝕜 (insert x s)) :
fderivWithin 𝕜 f (insert x s) (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
source
theorem HasFPowerSeriesOnBall.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : ↑‖y‖₊ < r) :
fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
source
theorem HasFPowerSeriesOnBall.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) :
HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r

If a function has a power series on a ball, then so does its derivative.

source
theorem HasFPowerSeriesWithinOnBall.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) (hu : UniqueDiffOn 𝕜 (insert x s)) :
HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r

If a function has a power series within a set on a ball, then so does its derivative.

source
theorem HasFPowerSeriesWithinOnBall.fderivWithin_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r

If a function has a power series within a set on a ball, then so does its derivative. For a version without completeness, but assuming that the function is analytic on the set `s`, see `HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn`.

source
theorem AnalyticAt.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} [CompleteSpace F] (h : AnalyticAt 𝕜 f x) :
AnalyticAt 𝕜 (fderiv 𝕜 f) x

If a function is analytic on a set `s`, so is its Fréchet derivative.

source
theorem AnalyticOnNhd.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s

If a function is analytic on a set `s`, so is its Fréchet derivative. See also `AnalyticOnNhd.fderiv_of_isOpen`, removing the completeness assumption but requiring the set to be open.

source
theorem AnalyticOnNhd.iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s

If a function is analytic on a set `s`, so are its successive Fréchet derivative. See also `AnalyticOnNhd.iteratedFDeriv_of_isOpen`, removing the completeness assumption but requiring the set to be open.

source
theorem AnalyticOnNhd.hasFTaylorSeriesUpToOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} [CompleteSpace F] (n : WithTop ℕ∞) (h : AnalyticOnNhd 𝕜 f s) :
HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s

If a function is analytic on a neighborhood of a set `s`, then it has a Taylor series given by the sequence of its derivatives. Note that, if the function were just analytic on `s`, then one would have to use instead the sequence of derivatives inside the set, as in `AnalyticOn.hasFTaylorSeriesUpToOn`.

source
theorem AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (n : WithTop ℕ∞) (h : AnalyticWithinAt 𝕜 f s x) :
∃ u ∈ nhdsWithin x (insert x s), ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn n f p u ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun (x : E) => p x i) u
source
theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} (h : HasFPowerSeriesWithinOnBall f p s x r) {f' : E →L[𝕜] F} {y : E} (hy : ↑‖y‖₊ < r) (h'y : x + y ∈ insert x s) (hf' : HasFDerivWithinAt f f' (insert x s) (x + y)) (hu : UniqueDiffOn 𝕜 (insert x s)) :
HasSum (fun (n : ℕ) => (p.derivSeries n) fun (x : Fin n) => y) f'

If a function has a power series `p` within a set of unique differentiability, inside a ball, and is differentiable at a point, then the derivative series of `p` is summable at a point, with sum the given differential. Note that this theorem does not require completeness of the space.

source
theorem HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} (hr : HasFPowerSeriesWithinOnBall f p s x r) (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r

If a function has a power series within a set on a ball, then so does its derivative. Version assuming that the function is analytic on `s`. For a version without this assumption but requiring that `F` is complete, see `HasFPowerSeriesWithinOnBall.fderivWithin_of_mem`.

source
theorem AnalyticOn.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s

If a function is analytic within a set with unique differentials, then so is its derivative. Note that this theorem does not require completeness of the space.

source
theorem AnalyticOn.iteratedFDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) (n : ℕ) :
AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s

If a function is analytic on a set `s`, so are its successive Fréchet derivative within this set. Note that this theorem does not require completeness of the space.

source
theorem AnalyticOn.hasFTaylorSeriesUpToOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {n : WithTop ℕ∞} (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
source
theorem AnalyticOn.exists_hasFTaylorSeriesUpToOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn ⊤ f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun (x : E) => p x i) s
source
theorem AnalyticOnNhd.fderiv_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) :
AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s
source
theorem AnalyticOnNhd.iteratedFDeriv_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) (n : ℕ) :
AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
source
theorem OpenPartialHomeomorph.analyticAt_symm' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {a : E} {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) (h : AnalyticAt 𝕜 (↑f) a) (h' : fderiv 𝕜 (↑f) a = ↑i) :
AnalyticAt 𝕜 (↑f.symm) (↑f a)

If an open partial homeomorphism `f` is analytic at a point `a`, with invertible derivative, then its inverse is analytic at `f a`.

source
theorem OpenPartialHomeomorph.analyticAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {a : F} {i : E ≃L[𝕜] F} (h0 : a ∈ f.target) (h : AnalyticAt 𝕜 (↑f) (↑f.symm a)) (h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i) :
AnalyticAt 𝕜 (↑f.symm) a

If an open partial homeomorphism `f` is analytic at a point `f.symm a`, with invertible derivative, then its inverse is analytic at `a`.

source
theorem HasFPowerSeriesAt.hasStrictDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜} (h : HasFPowerSeriesAt f p x) :
HasStrictDerivAt f ((p 1) fun (x : Fin 1) => 1) x
source
theorem HasFPowerSeriesAt.hasDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜} (h : HasFPowerSeriesAt f p x) :
HasDerivAt f ((p 1) fun (x : Fin 1) => 1) x
source
theorem HasFPowerSeriesAt.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜} (h : HasFPowerSeriesAt f p x) :
deriv f x = (p 1) fun (x : Fin 1) => 1
source
theorem AnalyticOnNhd.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
AnalyticOnNhd 𝕜 (deriv f) s

If a function is analytic on a set `s` in a complete space, so is its derivative.

source
theorem AnalyticOnNhd.deriv_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) :
AnalyticOnNhd 𝕜 (deriv f) s

If a function is analytic on an open set `s`, so is its derivative.

source
theorem AnalyticOnNhd.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
AnalyticOnNhd 𝕜 (deriv^[n] f) s

If a function is analytic on a set `s`, so are its successive derivatives.

source
theorem AnalyticAt.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [CompleteSpace F] (h : AnalyticAt 𝕜 f x) :
AnalyticAt 𝕜 (deriv f) x
source
theorem AnalyticAt.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [CompleteSpace F] (h : AnalyticAt 𝕜 f x) (n : ℕ) :
AnalyticAt 𝕜 (deriv^[n] f) x

The case of continuously polynomial functions. We get the same differentiability results as for analytic functions, but without the assumptions that `F` is complete.

source
theorem HasFiniteFPowerSeriesOnBall.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) :
DifferentiableOn 𝕜 f (EMetric.ball x r)
source
theorem HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : ↑‖y‖₊ < r) :
HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
source
theorem HasFiniteFPowerSeriesOnBall.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : ↑‖y‖₊ < r) :
HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
source
theorem HasFiniteFPowerSeriesOnBall.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : ↑‖y‖₊ < r) :
fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
source
theorem HasFiniteFPowerSeriesOnBall.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r) :
HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r

If a function has a finite power series on a ball, then so does its derivative.

source
theorem HasFiniteFPowerSeriesOnBall.fderiv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) :
HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r

If a function has a finite power series on a ball, then so does its derivative. This is a variant of `HasFiniteFPowerSeriesOnBall.fderiv` where the degree of `f` is `< n` and not `< n + 1`.

source
theorem CPolynomialOn.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : CPolynomialOn 𝕜 f s) :
CPolynomialOn 𝕜 (_root_.fderiv 𝕜 f) s

If a function is polynomial on a set `s`, so is its Fréchet derivative.

source
theorem CPolynomialOn.iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : CPolynomialOn 𝕜 f s) (n : ℕ) :
CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s

If a function is polynomial on a set `s`, so are its successive Fréchet derivative.

source
theorem CPolynomialOn.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (h : CPolynomialOn 𝕜 f s) :
CPolynomialOn 𝕜 (deriv f) s

If a function is polynomial on a set `s`, so is its derivative.

source
theorem CPolynomialOn.iterated_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (h : CPolynomialOn 𝕜 f s) (n : ℕ) :
CPolynomialOn 𝕜 (deriv^[n] f) s

If a function is polynomial on a set `s`, so are its successive derivatives.

source
theorem ContinuousMultilinearMap.changeOriginSeries_support {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {k l : ℕ} (h : k + l ≠ Fintype.card ι) :
f.toFormalMultilinearSeries.changeOriginSeries k l = 0
source
theorem ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) [DecidableEq ι] :
(continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x
source
theorem ContinuousMultilinearMap.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) [DecidableEq ι] :
HasStrictFDerivAt (⇑f) (f.linearDeriv x) x
source
theorem ContinuousMultilinearMap.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) [DecidableEq ι] :
HasFDerivAt (⇑f) (f.linearDeriv x) x
source
theorem ContinuousMultilinearMap.hasStrictFDerivAt_uncurry {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] [DecidableEq ι] (fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) :
HasStrictFDerivAt (fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) => fx.1 fx.2) ((apply 𝕜 E F fa.2).comp (ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) + (fa.1.linearDeriv fa.2).comp (ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))) fa
source
theorem HasStrictFDerivAt.continuousMultilinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [DecidableEq ι] {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F} {g : (i : ι) → G → E i} {f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : (i : ι) → G →L[𝕜] E i} (hf : HasStrictFDerivAt f f' x) (hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x) :
HasStrictFDerivAt (fun (x : G) => (f x) fun (x_1 : ι) => g x_1 x) ((ContinuousMultilinearMap.apply 𝕜 E F fun (x_1 : ι) => g x_1 x).comp f' + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (g' i)) x
source
theorem HasFDerivWithinAt.continuousMultilinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [DecidableEq ι] {s : Set G} {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F} {g : (i : ι) → G → E i} {f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : (i : ι) → G →L[𝕜] E i} (hf : HasFDerivWithinAt f f' s x) (hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x) :
HasFDerivWithinAt (fun (x : G) => (f x) fun (x_1 : ι) => g x_1 x) ((ContinuousMultilinearMap.apply 𝕜 E F fun (x_1 : ι) => g x_1 x).comp f' + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (g' i)) s x
source
theorem HasFDerivAt.continuousMultilinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [DecidableEq ι] {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F} {g : (i : ι) → G → E i} {f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : (i : ι) → G →L[𝕜] E i} (hf : HasFDerivAt f f' x) (hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x) :
HasFDerivAt (fun (x : G) => (f x) fun (x_1 : ι) => g x_1 x) ((ContinuousMultilinearMap.apply 𝕜 E F fun (x_1 : ι) => g x_1 x).comp f' + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (g' i)) x
source
theorem HasFDerivWithinAt.multilinear_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) [DecidableEq ι] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : (i : ι) → G → E i} {g' : (i : ι) → G →L[𝕜] E i} {s : Set G} {x : G} (hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x) :
HasFDerivWithinAt (fun (x : G) => f fun (i : ι) => g i x) (∑ i : ι, (f.toContinuousLinearMap (fun (j : ι) => g j x) i).comp (g' i)) s x

Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`. Version inside a set.

source
theorem HasFDerivAt.multilinear_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) [DecidableEq ι] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : (i : ι) → G → E i} {g' : (i : ι) → G →L[𝕜] E i} {x : G} (hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x) :
HasFDerivAt (fun (x : G) => f fun (i : ι) => g i x) (∑ i : ι, (f.toContinuousLinearMap (fun (j : ι) => g j x) i).comp (g' i)) x

Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`.

source
theorem ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) :
HasFTaylorSeriesUpTo ⊤ ⇑f fun (v : (i : ι) → E i) (n : ℕ) => f.iteratedFDeriv n v

A continuous multilinear function `f` admits a Taylor series, whose successive terms are given by `f.iteratedFDeriv n`. This is the point of the definition of `f.iteratedFDeriv`.

source
theorem ContinuousMultilinearMap.iteratedFDeriv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ) :
iteratedFDeriv 𝕜 n ⇑f = f.iteratedFDeriv n
source
theorem ContinuousMultilinearMap.norm_iteratedFDeriv_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ) (x : (i : ι) → E i) :
‖iteratedFDeriv 𝕜 n (⇑f) x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
source
theorem FormalMultilinearSeries.derivSeries_apply_diag {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (x : E) :
((p.derivSeries n) fun (x_1 : Fin n) => x) x = (n + 1) • (p (n + 1)) fun (x_1 : Fin (n + 1)) => x
source
@[simp]
theorem FormalMultilinearSeries.derivSeries_coeff_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 𝕜 F) (n : ℕ) :
(p.derivSeries.coeff n) 1 = (n + 1) • p.coeff (n + 1)
source
theorem HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) :
iteratedFDeriv 𝕜 0 f x = p 0
source
theorem HasFPowerSeriesOnBall.factorial_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) (y : E) [CompleteSpace F] (n : ℕ) :
(n.factorial • (p n) fun (x : Fin n) => y) = (iteratedFDeriv 𝕜 n f x) fun (x : Fin n) => y

The iterated derivative of an analytic function, on vectors `(y, ..., y)`, is given by `n!` times the `n`-th term in the power series. For a more general result giving the full iterated derivative as a sum over the permutations of `Fin n`, see `HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum`.

source
theorem HasFPowerSeriesOnBall.hasSum_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) [CompleteSpace F] [CharZero 𝕜] {y : E} (hy : y ∈ EMetric.ball 0 r) :
HasSum (fun (n : ℕ) => (↑n.factorial)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun (x : Fin n) => y) (f (x + y))

### Derivative of a linear map into multilinear maps #

source
theorem ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {G : ι → Type u_3} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] [Fintype ι] [DecidableEq ι] (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) (v : E × ((i : ι) → G i)) :
HasFDerivAt (fun (p : E × ((i : ι) → G i)) => (f p.1) p.2) ((f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i)) + ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i).comp ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))) v
source
theorem HasFDerivWithinAt.linear_multilinear_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {G : ι → Type u_3} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] [Fintype ι] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : (i : ι) → H → G i} {b' : (i : ι) → H →L[𝕜] G i} {s : Set H} {x : H} (ha : HasFDerivWithinAt a a' s x) (hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x) (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
HasFDerivWithinAt (fun (y : H) => (f (a y)) fun (i : ι) => b i y) ((f.flipMultilinear fun (i : ι) => b i x).comp a' + ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun (j : ι) => b j x) i).comp (b' i)) s x

Given `f` a linear map into multilinear maps, then the derivative of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by `f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`. Version inside a set.

source
theorem HasFDerivAt.linear_multilinear_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_2} {G : ι → Type u_3} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace 𝕜 (G i)] [Fintype ι] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : (i : ι) → H → G i} {b' : (i : ι) → H →L[𝕜] G i} {x : H} (ha : HasFDerivAt a a' x) (hb : ∀ (i : ι), HasFDerivAt (b i) (b' i) x) (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
HasFDerivAt (fun (y : H) => (f (a y)) fun (i : ι) => b i y) ((f.flipMultilinear fun (i : ι) => b i x).comp a' + ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun (j : ι) => b j x) i).comp (b' i)) x

Given `f` a linear map into multilinear maps, then the derivative of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by `f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`.