def IsFritzJohnMultiplier {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} (f : E → ℝ) (g : Fin m → E → ℝ) (xstar : E) (lambda0 : ℝ) (lambda : Fin m → ℝ) : Prop

A scalar lambda0 together with inequality multipliers lambda satisfies the Fritz-John conditions for the convex problem with objective f, constraints g, and candidate optimizer xstar when the multipliers are nonnegative, not all zero, satisfy the subdifferential stationarity condition, and obey complementary slackness.

@[simp]

theorem isFritzJohnMultiplier_iff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {xstar : E} {lambda0 : ℝ} {lambda : Fin m → ℝ} : IsFritzJohnMultiplier f g xstar lambda0 lambda ↔ 0 ≤ lambda0 ∧ (∀ (i : Fin m), 0 ≤ lambda i) ∧ (lambda0 ≠ 0 ∨ ∃ (i : Fin m), lambda i ≠ 0) ∧ 0 ∈ lambda0 • subdifferentialAt f xstar + ∑ i : Fin m, lambda i • subdifferentialAt (g i) xstar ∧ ∀ (i : Fin m), lambda i * g i xstar = 0

Unfolding IsFritzJohnMultiplier gives exactly the textbook Fritz-John multiplier conditions.

theorem IsFritzJohnMultiplier.lambda0_nonneg {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {xstar : E} {lambda0 : ℝ} {lambda : Fin m → ℝ} (h : IsFritzJohnMultiplier f g xstar lambda0 lambda) : 0 ≤ lambda0

Every Fritz-John multiplier has nonnegative scalar coefficient.

theorem IsFritzJohnMultiplier.nonneg {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {xstar : E} {lambda0 : ℝ} {lambda : Fin m → ℝ} (h : IsFritzJohnMultiplier f g xstar lambda0 lambda) (i : Fin m) : 0 ≤ lambda i

Every Fritz-John multiplier vector is componentwise nonnegative.

theorem IsFritzJohnMultiplier.not_all_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {xstar : E} {lambda0 : ℝ} {lambda : Fin m → ℝ} (h : IsFritzJohnMultiplier f g xstar lambda0 lambda) : lambda0 ≠ 0 ∨ ∃ (i : Fin m), lambda i ≠ 0

A Fritz-John multiplier family is not identically zero.

theorem IsFritzJohnMultiplier.stationarity {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {xstar : E} {lambda0 : ℝ} {lambda : Fin m → ℝ} (h : IsFritzJohnMultiplier f g xstar lambda0 lambda) : 0 ∈ lambda0 • subdifferentialAt f xstar + ∑ i : Fin m, lambda i • subdifferentialAt (g i) xstar

A Fritz-John multiplier family satisfies the subdifferential stationarity condition.

theorem IsFritzJohnMultiplier.complementary_slackness {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {xstar : E} {lambda0 : ℝ} {lambda : Fin m → ℝ} (h : IsFritzJohnMultiplier f g xstar lambda0 lambda) (i : Fin m) : lambda i * g i xstar = 0

A Fritz-John multiplier family satisfies complementary slackness.

theorem subdifferentialAtSubConstEq {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (c : ℝ) (x : E) : subdifferentialAt (fun (y : E) => f y - c) x = subdifferentialAt f x

Helper for Theorem 3.36: subtracting a scalar constant does not change the real-valued subdifferential at a point.

theorem isMinOnOptimalityResidualAtOptimalSolution {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} (f : E → ℝ) (g : Fin m → E → ℝ) (xstar : E) (hxstar : xstar ∈ inequality_feasible_set g) (hmin : IsMinOn f (inequality_feasible_set g) xstar) : IsMinOn (optimality_residual f (f xstar) g) Set.univ xstar

Helper for Theorem 3.36: an optimal feasible point globally minimizes the residual objective optimality_residual f (f xstar) g.

theorem residualPointwiseSupEqBranchFamily {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} (f : E → ℝ) (g : Fin m → E → ℝ) (xstar : E) : (fun (y : E) => ↑(optimality_residual f (f xstar) g y)) = fun (y : E) => ⨆ (i : Fin (m + 1)), ↑(optimality_residual_coordinates f (f xstar) g y i)

Helper for Theorem 3.36: the coerced residual objective is the pointwise supremum of its explicit residual-coordinate branch family.

theorem residualBranchSupAtOptimal_eq_zero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} (f : E → ℝ) (g : Fin m → E → ℝ) (xstar : E) (hxstar : xstar ∈ inequality_feasible_set g) : ⨆ (j : Fin (m + 1)), ↑(optimality_residual_coordinates f (f xstar) g xstar j) = 0

Helper for Theorem 3.36: at a feasible optimizer, the residual branch supremum at xstar is zero.

theorem zero_mem_convexHull_activeResidualSubdifferential {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} (f : E → ℝ) (g : Fin m → E → ℝ) (xstar : E) (hf : ConvexOn ℝ Set.univ f) (hg : ∀ (i : Fin m), ConvexOn ℝ Set.univ (g i)) (hxstar : xstar ∈ inequality_feasible_set g) (hmin : IsMinOn f (inequality_feasible_set g) xstar) : 0 ∈ (convexHull ℝ) (⋃ (i : { i : Fin (m + 1) // ↑(optimality_residual_coordinates f (f xstar) g xstar i) = ⨆ (j : Fin (m + 1)), ↑(optimality_residual_coordinates f (f xstar) g xstar j) }), ∂fun (y : E) => ↑(optimality_residual_coordinates f (f xstar) g y ↑i)(xstar))

Helper for Theorem 3.36: the zero dual vector belongs to the convex hull of the active subdifferentials of the residual branches at the optimal solution.

theorem exists_fritz_john_multipliers_of_isMinOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {m : ℕ} (f : E → ℝ) (g : Fin m → E → ℝ) (xstar : E) (hf : ConvexOn ℝ Set.univ f) (hg : ∀ (i : Fin m), ConvexOn ℝ Set.univ (g i)) (hxstar : xstar ∈ inequality_feasible_set g) (hmin : IsMinOn f (inequality_feasible_set g) xstar) : ∃ (lambda0 : ℝ) (lambda : Fin m → ℝ), IsFritzJohnMultiplier f g xstar lambda0 lambda

Theorem 3.36: Fritz-John necessary optimality conditions. If xstar is a feasible optimal solution of the convex problem min f x subject to g i x ≤ 0 for all i, then there exist nonnegative multipliers lambda0 and lambda that are not all zero and satisfy the subdifferential stationarity condition together with complementary slackness at xstar.