Analytic derivatives of multivariate polynomial families

The formal partial derivatives of a multivariate polynomial give its Fréchet derivative on the finite coordinate space over any nontrivially normed field. For a family of equations, with the product topology on its target, this identifies the analytic derivative with the linear map of TauCeti.jacobiMatrixAt. In particular the derivative is surjective exactly when the Jacobian matrix is, and the evaluation map of the family is analytic.

For real or complex Euclidean coordinate spaces, we also give the derivative applied to an arbitrary direction and to a standard coordinate direction.

theorem MvPolynomial.hasFDerivAt_eval {𝕜 : Type u_1} {σ : Type u_2} [NontriviallyNormedField 𝕜] [Fintype σ] (p : MvPolynomial σ 𝕜) (x : σ → 𝕜) : HasFDerivAt (fun (y : σ → 𝕜) => (eval y) p) (∑ j : σ, (eval x) ((pderiv j) p) • ContinuousLinearMap.proj j) x

The derivative of polynomial evaluation is the sum of its evaluated formal partial derivatives times the coordinate projections.

theorem MvPolynomial.fderiv_eval_euclidean_apply {σ : Type u_2} [Fintype σ] {𝕜 : Type u_4} [RCLike 𝕜] (p : MvPolynomial σ 𝕜) (x v : EuclideanSpace 𝕜 σ) : (fderiv 𝕜 (fun (y : EuclideanSpace 𝕜 σ) => (eval y.ofLp) p) x) v = ∑ i : σ, (eval x.ofLp) ((pderiv i) p) * v.ofLp i

The Fréchet derivative of polynomial evaluation on Euclidean space, applied to a direction, is the evaluated formal gradient paired with that direction.

@[simp]

theorem MvPolynomial.fderiv_eval_euclidean_single {σ : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [Finite σ] [DecidableEq σ] (p : MvPolynomial σ 𝕜) (x : EuclideanSpace 𝕜 σ) (i : σ) : (fderiv 𝕜 (fun (y : EuclideanSpace 𝕜 σ) => (eval y.ofLp) p) x) (EuclideanSpace.single i 1) = (eval x.ofLp) ((pderiv i) p)

Differentiating polynomial evaluation in a standard coordinate direction gives evaluation of the corresponding formal partial derivative. This also simplifies derivatives along EuclideanSpace.basisFun, whose simp normal form is EuclideanSpace.single i 1.

theorem TauCeti.hasFDerivAt_eval_family {𝕜 : Type u_1} {σ : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [Fintype σ] (p : ι → MvPolynomial σ 𝕜) (x : σ → 𝕜) : HasFDerivAt (fun (y : σ → 𝕜) (i : ι) => (MvPolynomial.eval y) (p i)) (ContinuousLinearMap.pi fun (i : ι) => ∑ j : σ, (MvPolynomial.eval x) ((MvPolynomial.pderiv j) (p i)) • ContinuousLinearMap.proj j) x

The analytic derivative of a polynomial family is its Jacobian matrix, viewed as a continuous linear map.

theorem TauCeti.fderiv_eval_family {𝕜 : Type u_1} {σ : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [Fintype σ] (p : ι → MvPolynomial σ 𝕜) (x : σ → 𝕜) : ↑(fderiv 𝕜 (fun (y : σ → 𝕜) (i : ι) => (MvPolynomial.eval y) (p i)) x) = (jacobiMatrixAt p x).mulVecLin

The Fréchet derivative of a polynomial family agrees with its formal Jacobian.

theorem TauCeti.surjective_fderiv_eval_family_iff {𝕜 : Type u_1} {σ : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [Fintype σ] (p : ι → MvPolynomial σ 𝕜) (x : σ → 𝕜) : Function.Surjective ⇑(fderiv 𝕜 (fun (y : σ → 𝕜) (i : ι) => (MvPolynomial.eval y) (p i)) x) ↔ Function.Surjective (jacobiMatrixAt p x).mulVec

The Fréchet derivative of a polynomial family is surjective exactly when its Jacobian matrix is.

theorem TauCeti.analyticOnNhd_eval_family {𝕜 : Type u_1} {σ : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [Fintype σ] [Fintype ι] (p : ι → MvPolynomial σ 𝕜) : AnalyticOnNhd 𝕜 (fun (x : σ → 𝕜) (i : ι) => (MvPolynomial.eval x) (p i)) Set.univ

The evaluation map of a polynomial family is analytic.