Quadratic forms are line (Gateaux) differentiable

In this file we prove that a quadratic form is line differentiable, with the line derivative given by the polar bilinear form. Note that this statement does not need topology on the domain. In particular, it applies to discontinuous quadratic forms on infinite dimensional spaces.

theorem QuadraticMap.hasLineDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : QuadraticMap 𝕜 E F) (a : E) (b : E) : HasLineDerivAt 𝕜 (⇑f) (QuadraticMap.polar (⇑f) a b) a b

theorem QuadraticMap.lineDifferentiableAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : QuadraticMap 𝕜 E F) (a : E) (b : E) : LineDifferentiableAt 𝕜 (⇑f) a b

@[simp]

theorem QuadraticMap.lineDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : QuadraticMap 𝕜 E F) : lineDeriv 𝕜 ⇑f = QuadraticMap.polar ⇑f