theorem isKuhnTuckerVectorForConcaveProgram_iff_neg_mem_concaveSubdifferentialAt_zero {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) (uStar : Fin m → ℝ) : IsKuhnTuckerVectorForConcaveProgram G uStar ↔ have h := perturbationFunctionOfConcaveProgram G; h 0 ≠ ⊤ ∧ h 0 ≠ ⊥ ∧ -uStar ∈ concaveSubdifferentialAt h 0

Theorem 6.30.8: for a concave bifunction G : ℝ^m → ℝ^n with perturbation function h = sup G, a vector u* ∈ ℝ^m is a Kuhn--Tucker vector for (Q) if and only if h(0) is finite and -u* ∈ ∂ h(0). In Lean, finiteness of h(0) is expressed by h 0 ≠ ⊤ and h 0 ≠ ⊥.

theorem corollary_6_30_1_30 : True

Corollary 30.1.30

theorem corollary_6_30_1_31 : True

Corollary 30.1.31

theorem proposition_6_30_1_32 : True

Proposition 30.1.32

theorem corollary_6_30_1_33 : True

Corollary 30.1.33

theorem fenchelYoung_inequality_and_eq_iff_mem_subdifferential {n : ℕ} (g : (Fin n → ℝ) → EReal) (hg : ProperConvexFunctionOn Set.univ g) (x xStar : Fin n → ℝ) : ↑(x ⬝ᵥ xStar) ≤ g x + fenchelConjugate n g xStar ∧ (g x + fenchelConjugate n g xStar = ↑(x ⬝ᵥ xStar) ↔ IsEuclideanSubgradientAt g x xStar)

Theorem 6.30.5: if g : ℝ^n → (-∞, +∞] is proper and convex, then for every x, x* ∈ ℝ^n one has the Fenchel--Young inequality ⟪x, x*⟫ ≤ g x + g*(x*). Moreover, equality holds if and only if x* is a Euclidean subgradient of g at x, equivalently x* ∈ ∂ g(x) under the standard identification of ℝ^n with its dual.

theorem mem_euclideanSubdifferentialAt_iff_mem_euclideanSubdifferentialAt_fenchelConjugate {n : ℕ} (g : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction g) (hproper : ProperConvexFunctionOn Set.univ g) (x xStar : Fin n → ℝ) : xStar ∈ euclideanSubdifferentialAt g x ↔ x ∈ euclideanSubdifferentialAt (fenchelConjugate n g) xStar

Theorem 6.30.6: if g : ℝ^n → (-∞, +∞] is a proper closed convex function and g* is its Fenchel conjugate, then for every x, x* ∈ ℝ^n one has x* ∈ ∂ g(x) if and only if x ∈ ∂ g*(x*), where both subdifferentials are interpreted in the Euclidean sense on Fin n → ℝ.

theorem corollary_6_30_5_2 : True

Corollary 30.5.2