theorem convex_lipschitz_tfae_subdifferential_norm_le_conjugate_domain_subset_closedBall {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (hf : ConvexOn ℝ Set.univ f) (L : NNReal) : [LipschitzWith L f, ∀ (x : E), ∀ g ∈ subdifferentialAt f x, ‖g‖ ≤ ↑L, (effective_domain fun (y : StrongDual ℝ E) => conjugate_function (fun (x : E) => ↑(f x)) ↑y) ⊆ Metric.closedBall 0 ↑L].TFAE

Theorem 4.13: for a convex real-valued function, the following are equivalent for the given Lipschitz bound L: (i) f is globally L-Lipschitz, (ii) every subgradient of f has norm at most L, and (iii) the effective domain of the conjugate f* is contained in the closed dual ball of radius L.

theorem lipschitzWith_iff_subdifferentialAt_norm_le_of_convexOn_univ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (hf : ConvexOn ℝ Set.univ f) (L : NNReal) : LipschitzWith L f ↔ ∀ (x : E), ∀ g ∈ subdifferentialAt f x, ‖g‖ ≤ ↑L

Companion bridge for Theorem 4.13: for a convex real-valued function, global LipschitzWith L is equivalent to the pointwise bound ‖g‖ ≤ L on every g ∈ subdifferentialAt f x.

theorem lipschitzWith_iff_conjugate_domain_subset_closedBall_of_convexOn_univ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (hf : ConvexOn ℝ Set.univ f) (L : NNReal) : LipschitzWith L f ↔ (effective_domain fun (y : StrongDual ℝ E) => conjugate_function (fun (x : E) => ↑(f x)) ↑y) ⊆ Metric.closedBall 0 ↑L

Companion bridge for Theorem 4.13: for a convex real-valued function, global LipschitzWith L is equivalent to the conjugate-domain inclusion effective_domain (fun y : StrongDual ℝ E ↦ conjugate_function (fun x ↦ (f x : EReal)) y) ⊆ closedBall 0 L.