theorem ContinuousLinearMap.strictGateauxDerivativeMonotoneOn_univ_iff_isStrictlyMonotone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (A : H →L[ℝ] H) : ERealFunction.StrictGateauxDerivativeMonotoneOn (fun (x : H) => (InnerProductSpace.toDual ℝ H) (A x)) Set.univ ↔ (↑A).IsStrictlyMonotone

For a linear derivative field on the whole space, strict Gâteaux monotonicity is exactly strict monotonicity of the underlying linear operator in the sense of Definition 2.23.

theorem quadraticForm_strictConvexOn_univ_iff_symmetricPart_positive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (A : H →L[ℝ] H) : (StrictConvexOn ℝ Set.univ fun (x : H) => inner ℝ x (A x)) ↔ ∀ (x : H), x ≠ 0 → 0 < inner ℝ ((A + ContinuousLinearMap.adjoint A) x) x

Example 17.11: for a bounded linear operator A on a real Hilbert space, the quadratic form x ↦ ⟪x, A x⟫_ℝ is strictly convex on H if and only if the quadratic form of the symmetric part A + A† is strictly positive on every nonzero vector.

theorem quadraticForm_strictConvexOn_univ_iff_symmetricPart_isStrictlyMonotone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (A : H →L[ℝ] H) : (StrictConvexOn ℝ Set.univ fun (x : H) => inner ℝ x (A x)) ↔ (↑(A + ContinuousLinearMap.adjoint A)).IsStrictlyMonotone

Canonical bridge for Example 17.11: the same strict convexity criterion can be expressed by saying that the symmetric part A + A† is strictly monotone.