Fréchet derivatives of quadratic maps

A quadratic map Q on a finite-dimensional normed space over a complete field is strictly differentiable, and its derivative at x is the linear map h ↦ polar Q x h (QuadraticMap.hasStrictFDerivAt). This upgrades Mathlib's line derivative of a quadratic map (QuadraticMap.hasLineDerivAt), which requires no topology on the domain, to a Fréchet derivative.

The proof writes Q as x ↦ B x x for a bilinear map B, which is possible because the space is free (LinearMap.BilinMap.toQuadraticMap_surjective); no assumption on the characteristic of the field is needed.

The file also builds a smooth function with prescribed value, derivative and constant symmetric second derivative at a point (TauCeti.exists_contDiff_apply_eq_fderiv_eq_fderiv_fderiv_eq).

theorem QuadraticMap.hasStrictFDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (Q : QuadraticMap 𝕜 E F) (x : E) : HasStrictFDerivAt (⇑Q) (LinearMap.toContinuousLinearMap (Q.polarBilin x)) x

A quadratic map on a finite-dimensional space is strictly differentiable, with derivative h ↦ polar Q x h at x.

theorem QuadraticMap.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (Q : QuadraticMap 𝕜 E F) (x : E) : HasFDerivAt (⇑Q) (LinearMap.toContinuousLinearMap (Q.polarBilin x)) x

A quadratic map on a finite-dimensional space has derivative h ↦ polar Q x h at x.

theorem QuadraticMap.differentiable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (Q : QuadraticMap 𝕜 E F) : Differentiable 𝕜 ⇑Q

A quadratic map on a finite-dimensional space is differentiable.

theorem QuadraticMap.fderiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (Q : QuadraticMap 𝕜 E F) (x h : E) : (fderiv 𝕜 (⇑Q) x) h = polar (⇑Q) x h

The derivative of a quadratic map on a finite-dimensional space at x is h ↦ polar Q x h.

theorem TauCeti.exists_contDiff_apply_eq_fderiv_eq_fderiv_fderiv_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (y : E) (c : F) (α : E →L[ℝ] F) (B : E →L[ℝ] E →L[ℝ] F) (hB : ∀ (u v : E), (B u) v = (B v) u) : ∃ (φ : E → F), ContDiff ℝ (↑⊤) φ ∧ φ y = c ∧ fderiv ℝ φ y = α ∧ ∀ (z : E), fderiv ℝ (fderiv ℝ φ) z = B

A smooth function with prescribed value, derivative and symmetric second derivative at a point, the latter constant: z ↦ c + α (z - y) + (1 / 2) • B (z - y) (z - y).