Frechet derivatives of analytic functions.

A function expressible as a power series at a point has a Frechet 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.
• PartialHomeomorph.analyticAt_symm : if a 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.

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.

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

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

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

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

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

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

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

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

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)

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)

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

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)

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)

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

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

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)

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)

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)

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)

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.

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.

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.

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.

@[deprecated AnalyticOnNhd.fderiv]

theorem AnalyticOn.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

Alias of AnalyticOnNhd.fderiv.

---

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.

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.

@[deprecated AnalyticOnNhd.iteratedFDeriv]

theorem AnalyticOn.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

Alias of AnalyticOnNhd.iteratedFDeriv.

---

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.

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.

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

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.

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.

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.

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

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

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

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

theorem PartialHomeomorph.analyticAt_symm' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : PartialHomeomorph 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 a partial homeomorphism f is analytic at a point a, with invertible derivative, then its inverse is analytic at f a.

theorem PartialHomeomorph.analyticAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : PartialHomeomorph 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 a partial homeomorphism f is analytic at a point f.symm a, with invertible derivative, then its inverse is analytic at a.

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

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

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

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.

@[deprecated AnalyticOnNhd.deriv]

theorem AnalyticOn.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

Alias of AnalyticOnNhd.deriv.

---

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

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.

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.

@[deprecated AnalyticOnNhd.iterated_deriv]

theorem AnalyticOn.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

Alias of AnalyticOnNhd.iterated_deriv.

---

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

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

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)

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)

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)

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.

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.

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 𝕜 (fderiv 𝕜 f) s

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

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 𝕜 (iteratedFDeriv 𝕜 n f) s

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

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.

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.

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

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

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

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.

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

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.

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

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)

theorem ContinuousMultilinearMap.cPolynomialAt {𝕜 : 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) : CPolynomialAt 𝕜 (⇑f) x

theorem ContinuousMultilinearMap.cPolyomialOn {𝕜 : 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) : CPolynomialOn 𝕜 ⇑f ⊤

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

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

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

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

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 (ContinuousLinearMap.fst 𝕜 E ((i : ι) → G i)) + ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i).comp ((ContinuousLinearMap.proj i).comp (ContinuousLinearMap.snd 𝕜 E ((i : ι) → G i)))) v

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.

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