theorem generalized_conditional_gradient_norm_eq_inner_add_value_add_conjugate {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f g : E → EReal) (x : E) : S[fun (y : E) => (f y).toReal, g](x) = ↑(inner ℝ (gradient (fun (y : E) => (f y).toReal) x) x) + g x + g∗ (-gradient (fun (y : E) => (f y).toReal) x)

Lemma 13.5: the generalized conditional-gradient norm rewrites as the affine term ⟪∇ f(x), x⟫ + g(x) plus the Fenchel conjugate value g∗(-∇ f(x)), where the gradient is taken for the real-valued map y ↦ (f y).toReal.