theorem hessianQuadraticForm_comp_affine {E : Type u} {E₁ : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup E₁] [InnerProductSpace ℝ E₁] [CompleteSpace E₁] (f : E₁ → ℝ) (g : E →ᴬ[ℝ] E₁) (x u : E) (hf : ContDiffAt ℝ 2 f (g x)) : inner ℝ u ((hessian (f ∘ ⇑g) x) u) = inner ℝ (g.contLinear u) ((hessian f (g x)) (g.contLinear u))

Lemma 5.1.1, owner form: the Hessian quadratic form of a continuous affine pullback f ∘ g at x in the direction u is the Hessian quadratic form of f at g x in the image direction g.contLinear u, provided f is C² at g x.

theorem hessianLocalNorm_comp_affine {E : Type u} {E₁ : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup E₁] [InnerProductSpace ℝ E₁] [CompleteSpace E₁] (f : E₁ → ℝ) (g : E →ᴬ[ℝ] E₁) (x u : E) (hf : ContDiffAt ℝ 2 f (g x)) : hessianLocalNorm (f ∘ ⇑g) x u = hessianLocalNorm f (g x) (g.contLinear u)

Lemma 5.1.1, local-norm form: the Hessian local norm of a continuous affine pullback f ∘ g at x in the direction u is the Hessian local norm of f at g x in the image direction g.contLinear u, provided f is C² at g x.

theorem thirdDirectionalDerivative_comp_affine {E : Type u} {E₁ : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] (f : E₁ → ℝ) (g : E →ᴬ[ℝ] E₁) (x u : E) : thirdDirectionalDerivative (f ∘ ⇑g) x u = thirdDirectionalDerivative f (g x) (g.contLinear u)

Lemma 5.1.1, third-derivative form: the third directional derivative of a continuous affine pullback f ∘ g at x along u is the third directional derivative of f at g x along g.contLinear u.