Convex analysis and calculus of variations

Convex functions and sets in analysis and optimization: Fenchel conjugates, polar sets, Moreau decomposition, convex projections, KKT conditions, gradient descent rates, Stampacchia, Tikhonov regularization, Euler–Lagrange, mountain pass and Ekeland principles; linear programming goes to convex geometry.

• Ekeland variational principle
• Euler–Lagrange equation
• Fenchel–Moreau theorem
• Gradient descent
• Lipschitz regularization by inf-convolution
• Moreau decomposition
• Mountain pass theorem
• Polar sets
• Stampacchia's theorem
• Tikhonov regularization

TheoremConvexity via the tangent-plane inequality#●ready to prove

Let \(E\) be a real Banach space, let \(X \subseteq E\) be an open convex set, and let \(f \colon E \to \mathbb{R}\) be twice continuously differentiable on \(X\). Then \(f\) is convex on \(X\) if and only if \(f(x) \ge f(a) + Df(a)(x - a)\) for all \(a, x \in X\), where \(Df(a)\) is the Fréchet derivative of \(f\) at \(a\) within \(X\).

public theorem_wanted convexOn_iff_forall_le_add_fderivWithin
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {X : Set E} (hXopen : IsOpen X) (hXconv : Convex ℝ X)
    {f : E → ℝ} (hf : ContDiffOn ℝ 2 f X) :
    ConvexOn ℝ X f ↔
      ∀ ⦃a⦄, a ∈ X → ∀ ⦃x⦄, x ∈ X →
        f x ≥ f a + (fderivWithin ℝ f X a) (x - a)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functional analysis; Measures, integration, derivative, holomorphy), problem ma_proofbench_l1_95.

TheoremKarush–Kuhn–Tucker conditions for inequality constraints#✓fully proved

Let \(E\) be a finite-dimensional real normed space, let \(f \colon E \to \mathbb{R}\) and \(g_1, \dots, g_m \colon E \to \mathbb{R}\), and let \(x \in E\) be a point at which \(f\) and every \(g_i\) are differentiable; write \(D\) for the Fréchet derivative at \(x\). Suppose that \(x\) is feasible, that is \(g_i(x) \le 0\) for every \(i\); that \(x\) is a local minimizer of \(f\) on the feasible set \(\{y \in E : g_i(y) \le 0 \text{ for every } i\}\); and that the derivatives \(Dg_i(x)\) of the active constraints, those \(i\) with \(g_i(x) = 0\), are linearly independent. Then there exist multipliers \(\lambda_1, \dots, \lambda_m \ge 0\) such that \(\lambda_i g_i(x) = 0\) for every \(i\) and \(Df(x) + \sum_{i=1}^m \lambda_i Dg_i(x) = 0\).

theorem karush_kuhn_tucker_inequality
    {m : ℕ} {f : E → ℝ} {g : Fin m → E → ℝ} {x : E}
    [FiniteDimensional ℝ E]
    (hf_diff : DifferentiableAt ℝ f x)
    (hg_diff : ∀ i, DifferentiableAt ℝ (g i) x)
    (hfeas : ∀ i, g i x ≤ 0)
    (hmin : IsLocalMinOn f {y | ∀ i, g i y ≤ 0} x)
    (hLICQ : LinearIndependent ℝ
      (fun i : {i : Fin m // g i x = 0} => fderiv ℝ (g i.val) x)) :
    ∃ lam : Fin m → ℝ, (∀ i, 0 ≤ lam i) ∧ (∀ i, lam i * g i x = 0) ∧
      fderiv ℝ f x + ∑ i : Fin m, lam i • fderiv ℝ (g i) x = 0

Sources

• W. Karush, Minima of Functions of Several Variables with Inequalities as Side Conditions (M.Sc. thesis, Univ. Chicago, 1939); H. W. Kuhn and A. W. Tucker, Nonlinear Programming, Proc. Second Berkeley Symposium (1951), 481–492, DOI 10.1525/9780520411586-036.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.