theorem fderiv_mem_subdifferentialAt_of_convexOn_univ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf_convex : ConvexOn ℝ Set.univ f) {x : E} (hdiff : DifferentiableAt ℝ f x) : fderiv ℝ f x ∈ subdifferentialAt f x

Helper for Theorem 5.26 direct proof repair: for a convex real-valued function on Set.univ, the Fréchet derivative at a differentiability point is a continuous-dual subgradient.

theorem strongConvexOn_toReal_conjugate_function_of_convex_is_l_smooth {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (σ : ℝ) (hσ : 0 < σ) (f : E → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_smooth : is_l_smooth_on f Set.univ (1 / σ).toNNReal) : StrongConvexOn (effective_domain (conjugate_function_strongDual (Function.toEReal f))) σ fun (y : StrongDual ℝ E) => (conjugate_function_strongDual (Function.toEReal f) y).toReal

Theorem 5.26 direct proof repair (1): if f : E → ℝ is convex and (1 / σ)-smooth on Set.univ, then its Fenchel conjugate on StrongDual ℝ E is σ-strongly convex on its effective domain.

theorem conjugate_function_finite_of_proper_closed_strongConvexOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (σ : ℝ) (hσ : 0 < σ) (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hclosed : LowerSemicontinuous f) (hstrong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (y : StrongDual ℝ E) : conjugate_function_strongDual f y ≠ ⊥ ∧ conjugate_function_strongDual f y < ⊤

If f : E → EReal is proper, closed, and σ-strongly convex, then its Fenchel conjugate on StrongDual ℝ E is finite everywhere.

theorem is_l_smooth_on_toReal_conjugate_function_strongDual_of_proper_closed_strongConvexOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (σ : ℝ) (hσ : 0 < σ) (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hclosed : LowerSemicontinuous f) (hstrong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) : is_l_smooth_on (fun (y : StrongDual ℝ E) => (conjugate_function_strongDual f y).toReal) Set.univ (1 / σ).toNNReal

Theorem 5.26 (2): if f : E → EReal is proper, closed, and σ-strongly convex, then the real-valued Fenchel conjugate on StrongDual ℝ E is (1 / σ)-smooth on Set.univ.