The derivative of a diagonal quadratic form

The diagonal quadratic form u ↦ c + (1/2) Σᵢ wᵢ uᵢ² on Fin n → ℝ has derivative v ↦ Σᵢ wᵢ uᵢ vᵢ at u. This is the normal form of a function at a nondegenerate critical point given by the Morse lemma.

Main results

• TauCeti.hasFDerivAt_diagonalQuadratic: the derivative of a diagonal quadratic form.

theorem TauCeti.hasFDerivAt_diagonalQuadratic {n : ℕ} (c : ℝ) (w u : Fin n → ℝ) : HasFDerivAt (fun (u : Fin n → ℝ) => c + 2⁻¹ * ∑ i : Fin n, w i * (u i * u i)) (∑ i : Fin n, (w i * u i) • ContinuousLinearMap.proj i) u

The diagonal quadratic form u ↦ c + (1/2) Σᵢ wᵢ uᵢ² has derivative v ↦ Σᵢ wᵢ uᵢ vᵢ.