theorem mem_subdifferential_iff_isMaxOn_affine_minus_conjugate {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (x : E) (y : Module.Dual ℝ E) : y ∈ ∂f(x) ↔ IsMaxOn (fun (y' : Module.Dual ℝ E) => ↑(y' x) - conjugate_function f y') Set.univ y

Helper for Theorem 4.12: y ∈ ∂ f(x) is equivalent to y maximizing y' ↦ y' x - f*(y') on the whole dual space.

theorem isMaxOn_univ_neg_iff_isMinOn_univ {X : Type u_1} (φ : X → EReal) (x : X) : IsMaxOn (fun (z : X) => -φ z) Set.univ x ↔ IsMinOn φ Set.univ x

Helper for Theorem 4.12: on Set.univ, maximizing the negation of an objective is equivalent to minimizing the original objective.

theorem subdifferential_eq_argmax_affine_minus_conjugate {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (x : E) : ∂f(x) = {y : Module.Dual ℝ E | IsMaxOn (fun (y' : Module.Dual ℝ E) => ↑(y' x) - conjugate_function f y') Set.univ y}

Theorem 4.12 (1): for a proper closed convex extended-real-valued function, the subdifferential at x is exactly the set of dual vectors maximizing y' ↦ y' x - f*(y').

theorem subdifferential_zero_eq_argmin_conjugate {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) : ∂f(0) = {y : Module.Dual ℝ E | IsMinOn (conjugate_function f) Set.univ y}

Theorem 4.12 (3): for a proper closed convex extended-real-valued function, the subdifferential at the origin is exactly the minimizer set of the conjugate f*.

theorem subdifferential_conjugate_eq_eval_image_argmax_affine_minus {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (y : Module.Dual ℝ E) : ∂conjugate_function f(y) = ⇑(Module.Dual.eval ℝ E) '' {x : E | IsMaxOn (fun (x' : E) => ↑(y x') - f x') Set.univ x}

Theorem 4.12 (2): for a proper closed convex extended-real-valued function, the subdifferential of the conjugate at y is the image under the canonical double-dual map Module.Dual.eval ℝ E of the maximizers of x' ↦ y x' - f(x').

theorem eval_mem_subdifferential_conjugate_iff_isMaxOn_affine_minus {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (y : Module.Dual ℝ E) (x : E) : (Module.Dual.eval ℝ E) x ∈ ∂conjugate_function f(y) ↔ IsMaxOn (fun (x' : E) => ↑(y x') - f x') Set.univ x

Companion theorem for Theorem 4.12 (2): the canonical double-dual image of x lies in ∂(f∗)(y) exactly when x maximizes x' ↦ y x' - f(x') on the whole space.

theorem subdifferential_conjugate_zero_eq_eval_image_argmin {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) : ∂conjugate_function f(0) = ⇑(Module.Dual.eval ℝ E) '' {x : E | IsMinOn f Set.univ x}

Theorem 4.12 (4): for a proper closed convex extended-real-valued function, at the zero dual vector the subdifferential of the conjugate is the canonical double-dual image of the minimizer set of f.