From c9486548a2b25cfe4e8727fe354bac09ce240838 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 17:43:03 +0100 Subject: [PATCH 1/6] feat: Lagrange duality for finitely many convex constraints under Slater's condition Co-Authored-By: Claude Code Co-Authored-By: Claude Opus 5.5 --- .../Analysis/Convex/LagrangeDuality.lean | 317 ++++++++++++++++++ 1 file changed, 317 insertions(+) create mode 100644 LMLExplore/Analysis/Convex/LagrangeDuality.lean diff --git a/LMLExplore/Analysis/Convex/LagrangeDuality.lean b/LMLExplore/Analysis/Convex/LagrangeDuality.lean new file mode 100644 index 00000000..4c0a3483 --- /dev/null +++ b/LMLExplore/Analysis/Convex/LagrangeDuality.lean @@ -0,0 +1,317 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.Analysis.LocallyConvex.Separation +public import Mathlib.Data.EReal.Basic + +/-! +# Lagrange duality for finitely many convex constraints + +Consider the convex program of minimizing `F x` over the points `x` of a convex set `C` that +satisfy finitely many convex constraints `h i x ≤ 0`, `i : ι`. Its Lagrangian is +`F x + ∑ i, π i * h i x` for multipliers `π : ι → ℝ≥0`, and its dual function is the infimum of the +Lagrangian over all of `C`, with the constraints dropped. Under **Slater's condition**, that some +`x₀ ∈ C` satisfies every constraint strictly, there is no duality gap: the value of the program is +the maximum over `π` of the dual function, and the minimizers of the program are the points that +minimize the Lagrangian of an optimal multiplier with complementary slackness [Lue69, §8.3, +Theorem 1; §8.6, Theorem 1]. + +The existence of multipliers only needs `F` and `h` to be jointly *convex-like* on `C` in the sense +of Fan [Fan53]: for `x, y ∈ C` and weights `a, b`, some `z ∈ C` has `F z` and every `h i z` below +the corresponding convex combinations of the values at `x` and `y`. It is stated in that form in +`LMLExplore.exists_forall_le_add_sum_of_convexLike`, which needs no linear structure on the domain +and so applies to convex sets of probability measures, which carry no real scalar multiplication. +Weak duality holds with no hypothesis; strong duality and the saddle point characterization are +stated for convex functions on a convex set. + +Values of the dual function are taken in `EReal`: the real infimum of a Lagrangian unbounded below +is the junk value `0`, for which weak duality fails. + +## Main statements + +* `LMLExplore.exists_forall_le_add_sum_of_convexLike`: under Slater's condition, every lower bound + of the objective on the feasible set is a lower bound of the Lagrangian on all of `C` for some + multiplier, for convex-like data on any type. +* `ConvexOn.exists_forall_le_add_sum_of_slater`: the same for convex functions on a convex set. +* `LMLExplore.iInf_add_sum_le_iInf`: weak duality, for every multiplier and with no hypothesis. +* `ConvexOn.exists_iInf_eq_iInf_add_of_slater`: strong duality with an optimal multiplier. +* `ConvexOn.iInf_eq_iSup_iInf_add_of_slater`: strong duality, the value of the program is the + supremum of the dual function. +* `ConvexOn.isMinOn_iff_exists_isMinOn_add_sum_of_slater`: the saddle point characterization of the + minimizers, by a multiplier for which they minimize the Lagrangian with complementary slackness. + +## Implementation notes + +The multiplier is produced by separating the point `(m, 0)`, for a lower bound `m` of `F` on the +feasible set, from the open convex set of the `v : Option ι → ℝ` lying strictly above +`(F x, h · x)` for some `x ∈ C`, with Mathlib's `geometric_hahn_banach_open_point`; Slater's +condition makes the coefficient of the objective in the separating functional nonzero. + +## References + +* [Lue69] D. G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 8. +* [Fan53] K. Fan, *Minimax theorems*, Proc. Natl. Acad. Sci. USA 39 (1953), 42–47. +-/ + +public section + +open Filter Set Topology +open scoped NNReal + +variable {X ι : Type*} {C : Set X} {F : X → ℝ} {h : ι → X → ℝ} + +namespace LMLExplore + +/-- The objective (`none`) and the constraints (`some i`) of the program, as one family. -/ +private def objConstr (F : X → ℝ) (h : ι → X → ℝ) (j : Option ι) (x : X) : ℝ := + j.elim (F x) fun i ↦ h i x + +/-- The points lying strictly above the joint values of the objective and the constraints at some +point of `C`. -/ +private def strictEpigraph (C : Set X) (F : X → ℝ) (h : ι → X → ℝ) : Set (Option ι → ℝ) := + {v | ∃ x ∈ C, ∀ j, objConstr F h j x < v j} + +private lemma isOpen_strictEpigraph [Finite ι] : IsOpen (strictEpigraph C F h) := by + have : strictEpigraph C F h = ⋃ x ∈ C, ⋂ j, {v : Option ι → ℝ | objConstr F h j x < v j} := by + ext v + simp [strictEpigraph] + rw [this] + exact isOpen_biUnion fun x _ ↦ isOpen_iInter_of_finite fun j ↦ + isOpen_lt continuous_const (continuous_apply j) + +/-- A convex combination of two strict inequalities is strict. -/ +private lemma combo_lt_combo {a b s t u w : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) + (hs : s < u) (ht : t < w) : a * s + b * t < a * u + b * w := by + rcases ha.eq_or_lt with rfl | ha + · obtain rfl : b = 1 := by linarith + linarith + · nlinarith [mul_lt_mul_of_pos_left hs ha, mul_le_mul_of_nonneg_left ht.le hb] + +private lemma convex_strictEpigraph + (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) : + Convex ℝ (strictEpigraph C F h) := by + rintro v ⟨x, hx, hxv⟩ w ⟨y, hy, hyw⟩ a b ha hb hab + obtain ⟨z, hz, hFz, hhz⟩ := hconv x hx y hy a b ha hb hab + refine ⟨z, hz, fun j ↦ ?_⟩ + have hz' : objConstr F h j z ≤ a * objConstr F h j x + b * objConstr F h j y := by + cases j <;> simp [objConstr, hFz, hhz] + simpa using hz'.trans_lt (combo_lt_combo ha hb hab (hxv j) (hyw j)) + +private lemma mem_strictEpigraph_of_le {v w : Option ι → ℝ} (hv : v ∈ strictEpigraph C F h) + (hvw : v ≤ w) : w ∈ strictEpigraph C F h := by + obtain ⟨x, hx, hxv⟩ := hv + exact ⟨x, hx, fun j ↦ (hxv j).trans_le (hvw j)⟩ + +/-- A functional below `f p` on the upward closed set `strictEpigraph C F h` is at most `f p` at +the joint values of the objective and the constraints at every point of `C`. -/ +private lemma apply_le_of_forall_lt {f : StrongDual ℝ (Option ι → ℝ)} {p : Option ι → ℝ} + (hf : ∀ v ∈ strictEpigraph C F h, f v < f p) {x : X} (hx : x ∈ C) : + f (fun j ↦ objConstr F h j x) ≤ f p := by + set v : Option ι → ℝ := fun j ↦ objConstr F h j x + -- `v + ε • 1` lies in `strictEpigraph C F h` for `ε > 0`, and tends to `v` as `ε → 0`. + have hlim : Tendsto (fun ε : ℝ ↦ f v + ε * f 1) (𝓝[>] 0) (𝓝 (f v)) := by + have : Tendsto (fun ε : ℝ ↦ f v + ε * f 1) (𝓝 0) (𝓝 (f v + 0 * f 1)) := + (continuous_const.add (continuous_id.mul continuous_const)).tendsto 0 + simpa using this.mono_left nhdsWithin_le_nhds + refine le_of_tendsto hlim (eventually_nhdsWithin_of_forall fun ε (hε : 0 < ε) ↦ ?_) + have := hf (v + ε • 1) ⟨x, hx, fun j ↦ by simpa [v] using hε⟩ + rw [map_add, map_smul, smul_eq_mul] at this + exact this.le + +/-- A functional below `f p` on the nonempty upward closed set `strictEpigraph C F h` is +nonpositive on nonnegative vectors. -/ +private lemma apply_nonpos_of_forall_lt {f : StrongDual ℝ (Option ι → ℝ)} {p a : Option ι → ℝ} + (hf : ∀ v ∈ strictEpigraph C F h, f v < f p) (ha : a ∈ strictEpigraph C F h) + {w : Option ι → ℝ} (hw : 0 ≤ w) : f w ≤ 0 := by + by_contra! hfw + -- Moving from `a` in the direction `w` reaches the level `f p` inside the set. + have ht : 0 ≤ (f p - f a) / f w := div_nonneg (sub_nonneg.2 (hf a ha).le) hfw.le + have := hf (a + ((f p - f a) / f w) • w) (mem_strictEpigraph_of_le ha fun k ↦ by + simpa using mul_nonneg ht (hw k)) + rw [map_add, map_smul, smul_eq_mul, div_mul_cancel₀ _ hfw.ne'] at this + linarith + +/-- **Fritz John multipliers** for convex-like data: if `m` is a lower bound of `F` on the feasible +set and `C` is nonempty, some nonzero nonpositive `c : Option ι → ℝ` has +`c none * F x + ∑ i, c (some i) * h i x ≤ c none * m` on `C`. -/ +private lemma exists_fritzJohn [Fintype ι] + (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + {x₀ : X} (hx₀ : x₀ ∈ C) {m : ℝ} (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : + ∃ c : Option ι → ℝ, c ≠ 0 ∧ (∀ j, c j ≤ 0) ∧ + ∀ x ∈ C, c none * F x + ∑ i, c (some i) * h i x ≤ c none * m := by + classical + -- The point `(m, 0)` lies outside the open convex set `strictEpigraph C F h`, so a continuous + -- linear functional `f` separates them. + let p : Option ι → ℝ := fun j ↦ j.elim m fun _ ↦ 0 + have hp : p ∉ strictEpigraph C F h := by + rintro ⟨x, hx, hxp⟩ + exact (hxp none).not_ge (hm x hx fun i ↦ (hxp (some i)).le) + obtain ⟨f, hf⟩ := geometric_hahn_banach_open_point (convex_strictEpigraph hconv) + isOpen_strictEpigraph hp + have ha₀ : (fun j ↦ objConstr F h j x₀ + 1) ∈ strictEpigraph C F h := + ⟨x₀, hx₀, fun j ↦ by simp⟩ + -- The coefficients `c j` of `f` in the standard basis. + let e : Option ι → Option ι → ℝ := fun j k ↦ if j = k then 1 else 0 + let c : Option ι → ℝ := fun j ↦ f (e j) + have hfc (v : Option ι → ℝ) : f v = c none * v none + ∑ i, c (some i) * v (some i) := by + rw [← Fintype.sum_option (fun j ↦ c j * v j)] + simpa [c, e, smul_eq_mul, mul_comm] using + LinearMap.pi_apply_eq_sum_univ (f : (Option ι → ℝ) →ₗ[ℝ] ℝ) v + refine ⟨c, fun hc ↦ ?_, fun j ↦ apply_nonpos_of_forall_lt hf ha₀ fun k ↦ by + by_cases hjk : j = k <;> simp [e, hjk], fun x hx ↦ ?_⟩ + · -- `f` is nonzero, since it is strictly below `f p` somewhere. + have := hf _ ha₀ + simp [hfc, hc] at this + · simpa [hfc, objConstr, p] using apply_le_of_forall_lt hf hx + +/-- **Lagrange multipliers under Slater's condition** [Lue69, §8.3, Theorem 1], for convex-like +data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`: for `x, y ∈ C` +and weights `a, b ≥ 0` with `a + b = 1`, some `z ∈ C` has `F z` and every `h i z` below the +corresponding convex combinations of the values at `x` and `y`. If some `x₀ ∈ C` satisfies +`h i x₀ < 0` for every `i` and `m` is a lower bound of `F` on the feasible set +`{x ∈ C | ∀ i, h i x ≤ 0}`, then some multiplier `π : ι → ℝ≥0` makes `m` a lower bound of the +Lagrangian `F x + ∑ i, π i * h i x` on all of `C`. + +No vector space structure on `X` is needed: this applies to convex sets of measures. For convex +functions on a convex set, see `ConvexOn.exists_forall_le_add_sum_of_slater`. +-/ +theorem exists_forall_le_add_sum_of_convexLike [Fintype ι] + (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {m : ℝ} + (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : + ∃ π : ι → ℝ≥0, ∀ x ∈ C, m ≤ F x + ∑ i, (π i : ℝ) * h i x := by + obtain ⟨x₀, hx₀, hx₀h⟩ := hslater + obtain ⟨c, hc, hc_nonpos, hcx⟩ := exists_fritzJohn hconv hx₀ hm + -- By Slater's condition the coefficient of the objective is negative: otherwise the terms + -- `c (some i) * h i x₀ ≥ 0` would have a nonpositive sum, so every coefficient would vanish. + have hc_neg : c none < 0 := by + refine (hc_nonpos none).lt_of_ne fun h0 ↦ hc ?_ + have hsum := hcx x₀ hx₀ + rw [h0, zero_mul, zero_mul, zero_add] at hsum + have hterm (i : ι) : 0 ≤ c (some i) * h i x₀ := + mul_nonneg_of_nonpos_of_nonpos (hc_nonpos _) (hx₀h i).le + have hzero (i : ι) : c (some i) = 0 := by + have := (Finset.sum_eq_zero_iff_of_nonneg fun i _ ↦ hterm i).1 + (le_antisymm hsum (Finset.sum_nonneg fun i _ ↦ hterm i)) i (Finset.mem_univ _) + exact (mul_eq_zero.1 this).resolve_right (hx₀h i).ne + ext (_ | i) + exacts [h0, hzero i] + -- Normalize the coefficient of the objective to `1`. + have hc0 : c none ≠ 0 := hc_neg.ne + have hL (x : X) (hx : x ∈ C) : m ≤ F x + ∑ i, c (some i) / c none * h i x := by + have hmul : c none * (F x + ∑ i, c (some i) / c none * h i x) = + c none * F x + ∑ i, c (some i) * h i x := by + rw [mul_add, Finset.mul_sum] + congr 1 + refine Finset.sum_congr rfl fun i _ ↦ ?_ + field_simp + rw [← mul_le_mul_left_of_neg hc_neg, hmul] + exact hcx x hx + exact ⟨fun i ↦ ⟨c (some i) / c none, div_nonneg_of_nonpos (hc_nonpos _) hc_neg.le⟩, hL⟩ + +/-- **Weak duality.** For every multiplier `π : ι → ℝ≥0`, the infimum over `C` of the Lagrangian +`F x + ∑ i, π i * h i x` is at most the infimum of `F` over the feasible set +`{x ∈ C | ∀ i, h i x ≤ 0}`, with values in `EReal`. -/ +theorem iInf_add_sum_le_iInf [Fintype ι] (π : ι → ℝ≥0) : + ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) ≤ + ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) := by + refine le_iInf₂ fun x ⟨hx, hxh⟩ ↦ (iInf₂_le x hx).trans (EReal.coe_le_coe_iff.2 ?_) + have : ∑ i, (π i : ℝ) * h i x ≤ 0 := + Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (π i).2 (hxh i) + linarith + +end LMLExplore + +namespace ConvexOn + +open LMLExplore + +variable [Fintype ι] {V : Type*} [AddCommMonoid V] [SMul ℝ V] {C : Set V} {F : V → ℝ} + {h : ι → V → ℝ} + +/-- **Lagrange multipliers under Slater's condition** [Lue69, §8.3, Theorem 1]. Let `F` and +finitely many `h i` be convex on a convex set `C`. If some `x₀ ∈ C` satisfies +`h i x₀ < 0` for every `i` and `m` is a lower bound of `F` on the feasible set +`{x ∈ C | ∀ i, h i x ≤ 0}`, then some multiplier `π : ι → ℝ≥0` makes `m` a lower bound of the +Lagrangian `F x + ∑ i, π i * h i x` on all of `C`. -/ +theorem exists_forall_le_add_sum_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {m : ℝ} + (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : + ∃ π : ι → ℝ≥0, ∀ x ∈ C, m ≤ F x + ∑ i, (π i : ℝ) * h i x := + exists_forall_le_add_sum_of_convexLike (fun x hx y hy a b ha hb hab ↦ + ⟨a • x + b • y, hF.1 hx hy ha hb hab, by simpa using hF.2 hx hy ha hb hab, + fun i ↦ by simpa using (hh i).2 hx hy ha hb hab⟩) hslater hm + +/-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1]. For `F` and +finitely many `h i` convex on a convex set `C`, if some `x₀ ∈ C` satisfies `h i x₀ < 0` for every +`i`, then some multiplier `π : ι → ℝ≥0` has dual value equal to the value of the program: the +infimum over `C` of the Lagrangian `F x + ∑ i, π i * h i x` is the infimum of `F` over +`{x ∈ C | ∀ i, h i x ≤ 0}`. Values are in `EReal`, so no boundedness is assumed: when `F` is +unbounded below on the feasible set, both sides are `⊥`. -/ +theorem exists_iInf_eq_iInf_add_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : + ∃ π : ι → ℝ≥0, ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = + ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by + set P := ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) + obtain ⟨x₀, hx₀, hx₀h⟩ := hslater + rcases eq_or_ne P ⊥ with hP | hP + · exact ⟨0, hP.trans (le_bot_iff.1 (hP ▸ iInf_add_sum_le_iInf 0)).symm⟩ + have hPtop : P ≠ ⊤ := + ((iInf₂_le x₀ ⟨hx₀, fun i ↦ (hx₀h i).le⟩).trans_lt (EReal.coe_lt_top _)).ne + obtain ⟨π, hπ⟩ := hF.exists_forall_le_add_sum_of_slater hh ⟨x₀, hx₀, hx₀h⟩ (m := P.toReal) + fun x hx hxh ↦ by + rw [← EReal.coe_le_coe_iff, EReal.coe_toReal hPtop hP] + exact iInf₂_le x ⟨hx, hxh⟩ + refine ⟨π, le_antisymm ?_ (iInf_add_sum_le_iInf π)⟩ + rw [← EReal.coe_toReal hPtop hP] + exact le_iInf₂ fun x hx ↦ EReal.coe_le_coe_iff.2 (hπ x hx) + +/-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1]. For `F` and +finitely many `h i` convex on a convex set `C`, if some `x₀ ∈ C` satisfies `h i x₀ < 0` for every +`i`, then the infimum of `F` over `{x ∈ C | ∀ i, h i x ≤ 0}` is the supremum over multipliers +`π : ι → ℝ≥0` of the infimum over `C` of the Lagrangian `F x + ∑ i, π i * h i x`, in `EReal`. The +supremum is attained (`ConvexOn.exists_iInf_eq_iInf_add_of_slater`). -/ +theorem iInf_eq_iSup_iInf_add_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : + ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = + ⨆ π : ι → ℝ≥0, ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by + obtain ⟨π, hπ⟩ := hF.exists_iInf_eq_iInf_add_of_slater hh hslater + exact le_antisymm (hπ.le.trans (le_iSup_of_le π le_rfl)) (iSup_le iInf_add_sum_le_iInf) + +/-- **Saddle point characterization of the minimizers** [Lue69, §8.3, Theorem 1; §8.4]. +For `F` and finitely many `h i` convex on a convex set `C`, with some `x₀ ∈ C` satisfying +`h i x₀ < 0` for every `i`, a feasible point `x` minimizes `F` over `{y ∈ C | ∀ i, h i y ≤ 0}` +exactly when some multiplier `π : ι → ℝ≥0` makes `x` a minimizer over `C` of the Lagrangian +`F y + ∑ i, π i * h i y`, with complementary slackness `π i * h i x = 0` for every `i`. -/ +theorem isMinOn_iff_exists_isMinOn_add_sum_of_slater (hF : ConvexOn ℝ C F) + (hh : ∀ i, ConvexOn ℝ C (h i)) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {x : V} (hx : x ∈ C) + (hxh : ∀ i, h i x ≤ 0) : + IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x ↔ + ∃ π : ι → ℝ≥0, IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x ∧ + ∀ i, (π i : ℝ) * h i x = 0 := by + have hterm (π : ι → ℝ≥0) (y : V) (hyh : ∀ i, h i y ≤ 0) (i : ι) : (π i : ℝ) * h i y ≤ 0 := + mul_nonpos_of_nonneg_of_nonpos (π i).2 (hyh i) + constructor + · intro hmin + obtain ⟨π, hπ⟩ := hF.exists_forall_le_add_sum_of_slater hh hslater (m := F x) + fun y hy hyh ↦ isMinOn_iff.1 hmin y ⟨hy, hyh⟩ + -- At `x` the sum of the nonpositive terms `π i * h i x` is nonnegative, hence each is zero. + have hsum : ∑ i, (π i : ℝ) * h i x = 0 := + le_antisymm (Finset.sum_nonpos fun i _ ↦ hterm π x hxh i) (by linarith [hπ x hx]) + have hslack (i : ι) : (π i : ℝ) * h i x = 0 := + (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm π x hxh i).1 hsum i (Finset.mem_univ _) + exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hsum] using hπ y hy, hslack⟩ + · rintro ⟨π, hmin, hslack⟩ + refine isMinOn_iff.2 fun y ⟨hy, hyh⟩ ↦ ?_ + have hle := isMinOn_iff.1 hmin y hy + simp only [hslack, Finset.sum_const_zero, add_zero] at hle + linarith [Finset.sum_nonpos fun i (_ : i ∈ Finset.univ) ↦ hterm π y hyh i] + +end ConvexOn From ab88fe272c4f54b8c2d0c1fe39e0195ad71c9c1e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:05:12 +0100 Subject: [PATCH 2/6] feat: state strong Lagrange duality and the saddle point theorem for convex-like data Add `exists_iInf_eq_iInf_add_of_convexLike`, `iInf_eq_iSup_iInf_add_of_convexLike` and `isMinOn_iff_exists_isMinOn_add_sum_of_convexLike` in `LMLExplore`, for Fan convex-like data on any type, and derive the `ConvexOn` versions from them in one line each. Co-Authored-By: Claude Code --- .../Analysis/Convex/LagrangeDuality.lean | 146 ++++++++++++------ 1 file changed, 100 insertions(+), 46 deletions(-) diff --git a/LMLExplore/Analysis/Convex/LagrangeDuality.lean b/LMLExplore/Analysis/Convex/LagrangeDuality.lean index 4c0a3483..9f63f3da 100644 --- a/LMLExplore/Analysis/Convex/LagrangeDuality.lean +++ b/LMLExplore/Analysis/Convex/LagrangeDuality.lean @@ -25,8 +25,9 @@ of Fan [Fan53]: for `x, y ∈ C` and weights `a, b`, some `z ∈ C` has `F z` an the corresponding convex combinations of the values at `x` and `y`. It is stated in that form in `LMLExplore.exists_forall_le_add_sum_of_convexLike`, which needs no linear structure on the domain and so applies to convex sets of probability measures, which carry no real scalar multiplication. -Weak duality holds with no hypothesis; strong duality and the saddle point characterization are -stated for convex functions on a convex set. +Strong duality and the saddle point characterization are stated in the same convex-like form, and +specialized to convex functions on a convex set in the `ConvexOn` namespace. Weak duality holds with +no hypothesis. Values of the dual function are taken in `EReal`: the real infimum of a Lagrangian unbounded below is the junk value `0`, for which weak duality fails. @@ -38,11 +39,13 @@ is the junk value `0`, for which weak duality fails. multiplier, for convex-like data on any type. * `ConvexOn.exists_forall_le_add_sum_of_slater`: the same for convex functions on a convex set. * `LMLExplore.iInf_add_sum_le_iInf`: weak duality, for every multiplier and with no hypothesis. -* `ConvexOn.exists_iInf_eq_iInf_add_of_slater`: strong duality with an optimal multiplier. -* `ConvexOn.iInf_eq_iSup_iInf_add_of_slater`: strong duality, the value of the program is the - supremum of the dual function. -* `ConvexOn.isMinOn_iff_exists_isMinOn_add_sum_of_slater`: the saddle point characterization of the - minimizers, by a multiplier for which they minimize the Lagrangian with complementary slackness. +* `LMLExplore.exists_iInf_eq_iInf_add_of_convexLike`: strong duality with an optimal multiplier, + for convex-like data; `ConvexOn.exists_iInf_eq_iInf_add_of_slater` for convex functions. +* `LMLExplore.iInf_eq_iSup_iInf_add_of_convexLike`: strong duality, the value of the program is the + supremum of the dual function; `ConvexOn.iInf_eq_iSup_iInf_add_of_slater` for convex functions. +* `LMLExplore.isMinOn_iff_exists_isMinOn_add_sum_of_convexLike`: the saddle point characterization + of the minimizers, by a multiplier for which they minimize the Lagrangian with complementary + slackness; `ConvexOn.isMinOn_iff_exists_isMinOn_add_sum_of_slater` for convex functions. ## Implementation notes @@ -227,15 +230,97 @@ theorem iInf_add_sum_le_iInf [Fintype ι] (π : ι → ℝ≥0) : Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (π i).2 (hxh i) linarith +/-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1], for convex-like +data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`, as in +`LMLExplore.exists_forall_le_add_sum_of_convexLike`. If some `x₀ ∈ C` satisfies `h i x₀ < 0` for +every `i`, then some multiplier `π : ι → ℝ≥0` has dual value equal to the value of the program: the +infimum over `C` of the Lagrangian `F x + ∑ i, π i * h i x` is the infimum of `F` over +`{x ∈ C | ∀ i, h i x ≤ 0}`. Values are in `EReal`, so no boundedness is assumed: when `F` is +unbounded below on the feasible set, both sides are `⊥`. -/ +theorem exists_iInf_eq_iInf_add_of_convexLike [Fintype ι] + (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : + ∃ π : ι → ℝ≥0, ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = + ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by + set P := ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) + obtain ⟨x₀, hx₀, hx₀h⟩ := hslater + rcases eq_or_ne P ⊥ with hP | hP + · exact ⟨0, hP.trans (le_bot_iff.1 (hP ▸ iInf_add_sum_le_iInf 0)).symm⟩ + have hPtop : P ≠ ⊤ := + ((iInf₂_le x₀ ⟨hx₀, fun i ↦ (hx₀h i).le⟩).trans_lt (EReal.coe_lt_top _)).ne + obtain ⟨π, hπ⟩ := exists_forall_le_add_sum_of_convexLike hconv ⟨x₀, hx₀, hx₀h⟩ (m := P.toReal) + fun x hx hxh ↦ by + rw [← EReal.coe_le_coe_iff, EReal.coe_toReal hPtop hP] + exact iInf₂_le x ⟨hx, hxh⟩ + refine ⟨π, le_antisymm ?_ (iInf_add_sum_le_iInf π)⟩ + rw [← EReal.coe_toReal hPtop hP] + exact le_iInf₂ fun x hx ↦ EReal.coe_le_coe_iff.2 (hπ x hx) + +/-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1], for convex-like +data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`, as in +`LMLExplore.exists_forall_le_add_sum_of_convexLike`. If some `x₀ ∈ C` satisfies `h i x₀ < 0` for +every `i`, then the infimum of `F` over `{x ∈ C | ∀ i, h i x ≤ 0}` is the supremum over multipliers +`π : ι → ℝ≥0` of the infimum over `C` of the Lagrangian `F x + ∑ i, π i * h i x`, in `EReal`. The +supremum is attained (`LMLExplore.exists_iInf_eq_iInf_add_of_convexLike`). -/ +theorem iInf_eq_iSup_iInf_add_of_convexLike [Fintype ι] + (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : + ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = + ⨆ π : ι → ℝ≥0, ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by + obtain ⟨π, hπ⟩ := exists_iInf_eq_iInf_add_of_convexLike hconv hslater + exact le_antisymm (hπ.le.trans (le_iSup_of_le π le_rfl)) (iSup_le iInf_add_sum_le_iInf) + +/-- **Saddle point characterization of the minimizers** [Lue69, §8.3, Theorem 1; §8.4], for +convex-like data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`, as +in `LMLExplore.exists_forall_le_add_sum_of_convexLike`, with some `x₀ ∈ C` satisfying `h i x₀ < 0` +for every `i`. A feasible point `x` minimizes `F` over `{y ∈ C | ∀ i, h i y ≤ 0}` exactly when some +multiplier `π : ι → ℝ≥0` makes `x` a minimizer over `C` of the Lagrangian +`F y + ∑ i, π i * h i y`, with complementary slackness `π i * h i x = 0` for every `i`. -/ +theorem isMinOn_iff_exists_isMinOn_add_sum_of_convexLike [Fintype ι] + (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {x : X} (hx : x ∈ C) (hxh : ∀ i, h i x ≤ 0) : + IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x ↔ + ∃ π : ι → ℝ≥0, IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x ∧ + ∀ i, (π i : ℝ) * h i x = 0 := by + have hterm (π : ι → ℝ≥0) (y : X) (hyh : ∀ i, h i y ≤ 0) (i : ι) : (π i : ℝ) * h i y ≤ 0 := + mul_nonpos_of_nonneg_of_nonpos (π i).2 (hyh i) + constructor + · intro hmin + obtain ⟨π, hπ⟩ := exists_forall_le_add_sum_of_convexLike hconv hslater (m := F x) + fun y hy hyh ↦ isMinOn_iff.1 hmin y ⟨hy, hyh⟩ + -- At `x` the sum of the nonpositive terms `π i * h i x` is nonnegative, hence each is zero. + have hsum : ∑ i, (π i : ℝ) * h i x = 0 := + le_antisymm (Finset.sum_nonpos fun i _ ↦ hterm π x hxh i) (by linarith [hπ x hx]) + have hslack (i : ι) : (π i : ℝ) * h i x = 0 := + (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm π x hxh i).1 hsum i (Finset.mem_univ _) + exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hsum] using hπ y hy, hslack⟩ + · rintro ⟨π, hmin, hslack⟩ + refine isMinOn_iff.2 fun y ⟨hy, hyh⟩ ↦ ?_ + have hle := isMinOn_iff.1 hmin y hy + simp only [hslack, Finset.sum_const_zero, add_zero] at hle + linarith [Finset.sum_nonpos fun i (_ : i ∈ Finset.univ) ↦ hterm π y hyh i] + end LMLExplore namespace ConvexOn open LMLExplore -variable [Fintype ι] {V : Type*} [AddCommMonoid V] [SMul ℝ V] {C : Set V} {F : V → ℝ} +variable {V : Type*} [AddCommMonoid V] [SMul ℝ V] {C : Set V} {F : V → ℝ} {h : ι → V → ℝ} +/-- Convex functions on a convex set are jointly convex-like there, witnessed by `a • x + b • y`. -/ +private lemma convexLike (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) : + ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y := + fun x hx y hy a b ha hb hab ↦ ⟨a • x + b • y, hF.1 hx hy ha hb hab, + by simpa using hF.2 hx hy ha hb hab, fun i ↦ by simpa using (hh i).2 hx hy ha hb hab⟩ + +variable [Fintype ι] + /-- **Lagrange multipliers under Slater's condition** [Lue69, §8.3, Theorem 1]. Let `F` and finitely many `h i` be convex on a convex set `C`. If some `x₀ ∈ C` satisfies `h i x₀ < 0` for every `i` and `m` is a lower bound of `F` on the feasible set @@ -245,9 +330,7 @@ theorem exists_forall_le_add_sum_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {m : ℝ} (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : ∃ π : ι → ℝ≥0, ∀ x ∈ C, m ≤ F x + ∑ i, (π i : ℝ) * h i x := - exists_forall_le_add_sum_of_convexLike (fun x hx y hy a b ha hb hab ↦ - ⟨a • x + b • y, hF.1 hx hy ha hb hab, by simpa using hF.2 hx hy ha hb hab, - fun i ↦ by simpa using (hh i).2 hx hy ha hb hab⟩) hslater hm + exists_forall_le_add_sum_of_convexLike (hF.convexLike hh) hslater hm /-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1]. For `F` and finitely many `h i` convex on a convex set `C`, if some `x₀ ∈ C` satisfies `h i x₀ < 0` for every @@ -258,20 +341,8 @@ unbounded below on the feasible set, both sides are `⊥`. -/ theorem exists_iInf_eq_iInf_add_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : ∃ π : ι → ℝ≥0, ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = - ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by - set P := ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) - obtain ⟨x₀, hx₀, hx₀h⟩ := hslater - rcases eq_or_ne P ⊥ with hP | hP - · exact ⟨0, hP.trans (le_bot_iff.1 (hP ▸ iInf_add_sum_le_iInf 0)).symm⟩ - have hPtop : P ≠ ⊤ := - ((iInf₂_le x₀ ⟨hx₀, fun i ↦ (hx₀h i).le⟩).trans_lt (EReal.coe_lt_top _)).ne - obtain ⟨π, hπ⟩ := hF.exists_forall_le_add_sum_of_slater hh ⟨x₀, hx₀, hx₀h⟩ (m := P.toReal) - fun x hx hxh ↦ by - rw [← EReal.coe_le_coe_iff, EReal.coe_toReal hPtop hP] - exact iInf₂_le x ⟨hx, hxh⟩ - refine ⟨π, le_antisymm ?_ (iInf_add_sum_le_iInf π)⟩ - rw [← EReal.coe_toReal hPtop hP] - exact le_iInf₂ fun x hx ↦ EReal.coe_le_coe_iff.2 (hπ x hx) + ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := + exists_iInf_eq_iInf_add_of_convexLike (hF.convexLike hh) hslater /-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1]. For `F` and finitely many `h i` convex on a convex set `C`, if some `x₀ ∈ C` satisfies `h i x₀ < 0` for every @@ -281,9 +352,8 @@ supremum is attained (`ConvexOn.exists_iInf_eq_iInf_add_of_slater`). -/ theorem iInf_eq_iSup_iInf_add_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = - ⨆ π : ι → ℝ≥0, ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by - obtain ⟨π, hπ⟩ := hF.exists_iInf_eq_iInf_add_of_slater hh hslater - exact le_antisymm (hπ.le.trans (le_iSup_of_le π le_rfl)) (iSup_le iInf_add_sum_le_iInf) + ⨆ π : ι → ℝ≥0, ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := + iInf_eq_iSup_iInf_add_of_convexLike (hF.convexLike hh) hslater /-- **Saddle point characterization of the minimizers** [Lue69, §8.3, Theorem 1; §8.4]. For `F` and finitely many `h i` convex on a convex set `C`, with some `x₀ ∈ C` satisfying @@ -295,23 +365,7 @@ theorem isMinOn_iff_exists_isMinOn_add_sum_of_slater (hF : ConvexOn ℝ C F) (hxh : ∀ i, h i x ≤ 0) : IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x ↔ ∃ π : ι → ℝ≥0, IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x ∧ - ∀ i, (π i : ℝ) * h i x = 0 := by - have hterm (π : ι → ℝ≥0) (y : V) (hyh : ∀ i, h i y ≤ 0) (i : ι) : (π i : ℝ) * h i y ≤ 0 := - mul_nonpos_of_nonneg_of_nonpos (π i).2 (hyh i) - constructor - · intro hmin - obtain ⟨π, hπ⟩ := hF.exists_forall_le_add_sum_of_slater hh hslater (m := F x) - fun y hy hyh ↦ isMinOn_iff.1 hmin y ⟨hy, hyh⟩ - -- At `x` the sum of the nonpositive terms `π i * h i x` is nonnegative, hence each is zero. - have hsum : ∑ i, (π i : ℝ) * h i x = 0 := - le_antisymm (Finset.sum_nonpos fun i _ ↦ hterm π x hxh i) (by linarith [hπ x hx]) - have hslack (i : ι) : (π i : ℝ) * h i x = 0 := - (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm π x hxh i).1 hsum i (Finset.mem_univ _) - exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hsum] using hπ y hy, hslack⟩ - · rintro ⟨π, hmin, hslack⟩ - refine isMinOn_iff.2 fun y ⟨hy, hyh⟩ ↦ ?_ - have hle := isMinOn_iff.1 hmin y hy - simp only [hslack, Finset.sum_const_zero, add_zero] at hle - linarith [Finset.sum_nonpos fun i (_ : i ∈ Finset.univ) ↦ hterm π y hyh i] + ∀ i, (π i : ℝ) * h i x = 0 := + isMinOn_iff_exists_isMinOn_add_sum_of_convexLike (hF.convexLike hh) hslater hx hxh end ConvexOn From 7b26a31d91d6e8ca2b4e2f7091752365ef5cf6c6 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:25:51 +0100 Subject: [PATCH 3/6] feat: expose the Fritz John multiplier theorem for convex-like data Make the private `exists_fritzJohn` public as `LMLExplore.exists_ne_zero_forall_le_of_convexLike`, with nonnegative multipliers, no nonemptiness hypothesis, a docstring and a Main statements entry. Co-Authored-By: Claude Code --- .../Analysis/Convex/LagrangeDuality.lean | 60 ++++++++++++------- 1 file changed, 37 insertions(+), 23 deletions(-) diff --git a/LMLExplore/Analysis/Convex/LagrangeDuality.lean b/LMLExplore/Analysis/Convex/LagrangeDuality.lean index 9f63f3da..01fc47d3 100644 --- a/LMLExplore/Analysis/Convex/LagrangeDuality.lean +++ b/LMLExplore/Analysis/Convex/LagrangeDuality.lean @@ -34,6 +34,8 @@ is the junk value `0`, for which weak duality fails. ## Main statements +* `LMLExplore.exists_ne_zero_forall_le_of_convexLike`: Fritz John multipliers for convex-like data, + with no constraint qualification. * `LMLExplore.exists_forall_le_add_sum_of_convexLike`: under Slater's condition, every lower bound of the objective on the feasible set is a lower bound of the Lagrangian on all of `C` for some multiplier, for convex-like data on any type. @@ -139,16 +141,25 @@ private lemma apply_nonpos_of_forall_lt {f : StrongDual ℝ (Option ι → ℝ)} rw [map_add, map_smul, smul_eq_mul, div_mul_cancel₀ _ hfw.ne'] at this linarith -/-- **Fritz John multipliers** for convex-like data: if `m` is a lower bound of `F` on the feasible -set and `C` is nonempty, some nonzero nonpositive `c : Option ι → ℝ` has -`c none * F x + ∑ i, c (some i) * h i x ≤ c none * m` on `C`. -/ -private lemma exists_fritzJohn [Fintype ι] +/-- **Fritz John multipliers** for convex-like data, with no constraint qualification. Let `F` and +finitely many `h i` be jointly convex-like on a set `C`, as in +`LMLExplore.exists_forall_le_add_sum_of_convexLike`. If `m` is a lower bound of `F` on the feasible +set `{x ∈ C | ∀ i, h i x ≤ 0}`, then some nonzero `c : Option ι → ℝ` with nonnegative entries, the +coefficient `c none` of the objective and the coefficients `c (some i)` of the constraints, has +`c none * m ≤ c none * F x + ∑ i, c (some i) * h i x` for every `x ∈ C`. + +Under Slater's condition `c none` is positive, which gives +`LMLExplore.exists_forall_le_add_sum_of_convexLike`. -/ +theorem exists_ne_zero_forall_le_of_convexLike [Fintype ι] (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) - {x₀ : X} (hx₀ : x₀ ∈ C) {m : ℝ} (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : - ∃ c : Option ι → ℝ, c ≠ 0 ∧ (∀ j, c j ≤ 0) ∧ - ∀ x ∈ C, c none * F x + ∑ i, c (some i) * h i x ≤ c none * m := by + {m : ℝ} (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : + ∃ c : Option ι → ℝ, c ≠ 0 ∧ (∀ j, 0 ≤ c j) ∧ + ∀ x ∈ C, c none * m ≤ c none * F x + ∑ i, c (some i) * h i x := by classical + rcases C.eq_empty_or_nonempty with rfl | ⟨x₀, hx₀⟩ + · exact ⟨fun _ ↦ 1, fun h1 ↦ one_ne_zero (congrFun h1 none), fun _ ↦ zero_le_one, + fun x hx ↦ absurd hx (notMem_empty x)⟩ -- The point `(m, 0)` lies outside the open convex set `strictEpigraph C F h`, so a continuous -- linear functional `f` separates them. let p : Option ι → ℝ := fun j ↦ j.elim m fun _ ↦ 0 @@ -159,19 +170,21 @@ private lemma exists_fritzJohn [Fintype ι] isOpen_strictEpigraph hp have ha₀ : (fun j ↦ objConstr F h j x₀ + 1) ∈ strictEpigraph C F h := ⟨x₀, hx₀, fun j ↦ by simp⟩ - -- The coefficients `c j` of `f` in the standard basis. + -- The coefficients `c j` of `f` in the standard basis; the multipliers are `-c`. let e : Option ι → Option ι → ℝ := fun j k ↦ if j = k then 1 else 0 let c : Option ι → ℝ := fun j ↦ f (e j) have hfc (v : Option ι → ℝ) : f v = c none * v none + ∑ i, c (some i) * v (some i) := by rw [← Fintype.sum_option (fun j ↦ c j * v j)] simpa [c, e, smul_eq_mul, mul_comm] using LinearMap.pi_apply_eq_sum_univ (f : (Option ι → ℝ) →ₗ[ℝ] ℝ) v - refine ⟨c, fun hc ↦ ?_, fun j ↦ apply_nonpos_of_forall_lt hf ha₀ fun k ↦ by - by_cases hjk : j = k <;> simp [e, hjk], fun x hx ↦ ?_⟩ + refine ⟨-c, neg_ne_zero.2 fun hc ↦ ?_, fun j ↦ neg_nonneg.2 <| + apply_nonpos_of_forall_lt hf ha₀ fun k ↦ by by_cases hjk : j = k <;> simp [e, hjk], + fun x hx ↦ ?_⟩ · -- `f` is nonzero, since it is strictly below `f p` somewhere. have := hf _ ha₀ simp [hfc, hc] at this - · simpa [hfc, objConstr, p] using apply_le_of_forall_lt hf hx + · simp only [Pi.neg_apply, neg_mul, Finset.sum_neg_distrib, ← neg_add, neg_le_neg_iff] + simpa [hfc, objConstr, p] using apply_le_of_forall_lt hf hx /-- **Lagrange multipliers under Slater's condition** [Lue69, §8.3, Theorem 1], for convex-like data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`: for `x, y ∈ C` @@ -191,23 +204,23 @@ theorem exists_forall_le_add_sum_of_convexLike [Fintype ι] (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : ∃ π : ι → ℝ≥0, ∀ x ∈ C, m ≤ F x + ∑ i, (π i : ℝ) * h i x := by obtain ⟨x₀, hx₀, hx₀h⟩ := hslater - obtain ⟨c, hc, hc_nonpos, hcx⟩ := exists_fritzJohn hconv hx₀ hm - -- By Slater's condition the coefficient of the objective is negative: otherwise the terms - -- `c (some i) * h i x₀ ≥ 0` would have a nonpositive sum, so every coefficient would vanish. - have hc_neg : c none < 0 := by - refine (hc_nonpos none).lt_of_ne fun h0 ↦ hc ?_ + obtain ⟨c, hc, hc_nonneg, hcx⟩ := exists_ne_zero_forall_le_of_convexLike hconv hm + -- By Slater's condition the coefficient of the objective is positive: otherwise the terms + -- `c (some i) * h i x₀ ≤ 0` would have a nonnegative sum, so every coefficient would vanish. + have hc_pos : 0 < c none := by + refine (hc_nonneg none).lt_of_ne' fun h0 ↦ hc ?_ have hsum := hcx x₀ hx₀ rw [h0, zero_mul, zero_mul, zero_add] at hsum - have hterm (i : ι) : 0 ≤ c (some i) * h i x₀ := - mul_nonneg_of_nonpos_of_nonpos (hc_nonpos _) (hx₀h i).le + have hterm (i : ι) : c (some i) * h i x₀ ≤ 0 := + mul_nonpos_of_nonneg_of_nonpos (hc_nonneg _) (hx₀h i).le have hzero (i : ι) : c (some i) = 0 := by - have := (Finset.sum_eq_zero_iff_of_nonneg fun i _ ↦ hterm i).1 - (le_antisymm hsum (Finset.sum_nonneg fun i _ ↦ hterm i)) i (Finset.mem_univ _) + have := (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm i).1 + (le_antisymm (Finset.sum_nonpos fun i _ ↦ hterm i) hsum) i (Finset.mem_univ _) exact (mul_eq_zero.1 this).resolve_right (hx₀h i).ne ext (_ | i) exacts [h0, hzero i] -- Normalize the coefficient of the objective to `1`. - have hc0 : c none ≠ 0 := hc_neg.ne + have hc0 : c none ≠ 0 := hc_pos.ne' have hL (x : X) (hx : x ∈ C) : m ≤ F x + ∑ i, c (some i) / c none * h i x := by have hmul : c none * (F x + ∑ i, c (some i) / c none * h i x) = c none * F x + ∑ i, c (some i) * h i x := by @@ -215,9 +228,10 @@ theorem exists_forall_le_add_sum_of_convexLike [Fintype ι] congr 1 refine Finset.sum_congr rfl fun i _ ↦ ?_ field_simp - rw [← mul_le_mul_left_of_neg hc_neg, hmul] + refine le_of_mul_le_mul_left ?_ hc_pos + rw [hmul] exact hcx x hx - exact ⟨fun i ↦ ⟨c (some i) / c none, div_nonneg_of_nonpos (hc_nonpos _) hc_neg.le⟩, hL⟩ + exact ⟨fun i ↦ ⟨c (some i) / c none, div_nonneg (hc_nonneg _) hc_pos.le⟩, hL⟩ /-- **Weak duality.** For every multiplier `π : ι → ℝ≥0`, the infimum over `C` of the Lagrangian `F x + ∑ i, π i * h i x` is at most the infimum of `F` over the feasible set From c3a0e083adcb42a3f8d1ffa52f0675132a854283 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:41:41 +0100 Subject: [PATCH 4/6] feat: state the saddle point sufficiency direction with no hypothesis MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `LMLExplore.isMinOn_of_isMinOn_add_sum`: a minimizer over `C` of a Lagrangian with complementary slackness minimizes the objective over the feasible set, with no convexity or constraint qualification. The `←` direction of the saddle point characterizations now uses it. Co-Authored-By: Claude Code --- .../Analysis/Convex/LagrangeDuality.lean | 25 ++++++++++++++----- 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/LMLExplore/Analysis/Convex/LagrangeDuality.lean b/LMLExplore/Analysis/Convex/LagrangeDuality.lean index 01fc47d3..fe3f71b3 100644 --- a/LMLExplore/Analysis/Convex/LagrangeDuality.lean +++ b/LMLExplore/Analysis/Convex/LagrangeDuality.lean @@ -26,8 +26,8 @@ the corresponding convex combinations of the values at `x` and `y`. It is stated `LMLExplore.exists_forall_le_add_sum_of_convexLike`, which needs no linear structure on the domain and so applies to convex sets of probability measures, which carry no real scalar multiplication. Strong duality and the saddle point characterization are stated in the same convex-like form, and -specialized to convex functions on a convex set in the `ConvexOn` namespace. Weak duality holds with -no hypothesis. +specialized to convex functions on a convex set in the `ConvexOn` namespace. Weak duality, and the +sufficiency of the saddle point condition, hold with no hypothesis. Values of the dual function are taken in `EReal`: the real infimum of a Lagrangian unbounded below is the junk value `0`, for which weak duality fails. @@ -41,6 +41,8 @@ is the junk value `0`, for which weak duality fails. multiplier, for convex-like data on any type. * `ConvexOn.exists_forall_le_add_sum_of_slater`: the same for convex functions on a convex set. * `LMLExplore.iInf_add_sum_le_iInf`: weak duality, for every multiplier and with no hypothesis. +* `LMLExplore.isMinOn_of_isMinOn_add_sum`: a minimizer of a Lagrangian with complementary + slackness minimizes the program, with no hypothesis. * `LMLExplore.exists_iInf_eq_iInf_add_of_convexLike`: strong duality with an optimal multiplier, for convex-like data; `ConvexOn.exists_iInf_eq_iInf_add_of_slater` for convex functions. * `LMLExplore.iInf_eq_iSup_iInf_add_of_convexLike`: strong duality, the value of the program is the @@ -244,6 +246,20 @@ theorem iInf_add_sum_le_iInf [Fintype ι] (π : ι → ℝ≥0) : Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (π i).2 (hxh i) linarith +/-- **Sufficiency of the saddle point condition** [Lue69, §8.4]. If `x` minimizes over `C` the +Lagrangian `F y + ∑ i, π i * h i y` of some multiplier `π : ι → ℝ≥0`, with complementary slackness +`π i * h i x = 0` for every `i`, then `x` minimizes `F` over `{y ∈ C | ∀ i, h i y ≤ 0}`. No +convexity or constraint qualification is needed. -/ +theorem isMinOn_of_isMinOn_add_sum [Fintype ι] {π : ι → ℝ≥0} {x : X} + (hmin : IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x) + (hslack : ∀ i, (π i : ℝ) * h i x = 0) : IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x := by + refine isMinOn_iff.2 fun y ⟨hy, hyh⟩ ↦ ?_ + have hle := isMinOn_iff.1 hmin y hy + simp only [hslack, Finset.sum_const_zero, add_zero] at hle + have hsum : ∑ i, (π i : ℝ) * h i y ≤ 0 := + Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (π i).2 (hyh i) + linarith + /-- **Strong Lagrange duality under Slater's condition** [Lue69, §8.6, Theorem 1], for convex-like data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`, as in `LMLExplore.exists_forall_le_add_sum_of_convexLike`. If some `x₀ ∈ C` satisfies `h i x₀ < 0` for @@ -312,10 +328,7 @@ theorem isMinOn_iff_exists_isMinOn_add_sum_of_convexLike [Fintype ι] (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm π x hxh i).1 hsum i (Finset.mem_univ _) exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hsum] using hπ y hy, hslack⟩ · rintro ⟨π, hmin, hslack⟩ - refine isMinOn_iff.2 fun y ⟨hy, hyh⟩ ↦ ?_ - have hle := isMinOn_iff.1 hmin y hy - simp only [hslack, Finset.sum_const_zero, add_zero] at hle - linarith [Finset.sum_nonpos fun i (_ : i ∈ Finset.univ) ↦ hterm π y hyh i] + exact isMinOn_of_isMinOn_add_sum hmin hslack end LMLExplore From e35ea2c63acc4221f718577a6fa538a76fce2765 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:26:55 +0100 Subject: [PATCH 5/6] refactor: factor out complementary slackness and move the saddle point sufficiency lemma to IsMinOn Rename LMLExplore.isMinOn_of_isMinOn_add_sum_mul (new in this PR) to IsMinOn.of_add_sum_mul, factor the nonpositive-terms-with-nonnegative-sum argument into private lemmas used at both sites, and fix the docstring of exists_iInf_eq_iInf_add_of_convexLike. Co-Authored-By: Claude Code --- .../Analysis/Convex/LagrangeDuality.lean | 52 ++++++++++--------- 1 file changed, 28 insertions(+), 24 deletions(-) diff --git a/LMLExplore/Analysis/Convex/LagrangeDuality.lean b/LMLExplore/Analysis/Convex/LagrangeDuality.lean index 1c3f67fb..7253f568 100644 --- a/LMLExplore/Analysis/Convex/LagrangeDuality.lean +++ b/LMLExplore/Analysis/Convex/LagrangeDuality.lean @@ -43,7 +43,7 @@ of a bet `1 + ∑ i, π i * g i`. ## Main statements * `LMLExplore.iSup_iInf_add_le_iInf`: weak duality in `EReal`, with no hypothesis. -* `LMLExplore.isMinOn_of_isMinOn_add_sum_mul`: a minimizer of a Lagrangian with complementary +* `IsMinOn.of_add_sum_mul`: a minimizer of a Lagrangian with complementary slackness minimizes the program, with no hypothesis. * `LMLExplore.exists_ne_zero_forall_le_of_convexLike`: Fritz John multipliers for convex-like data, with no constraint qualification. @@ -87,11 +87,21 @@ variable {X ι : Type*} {C : Set X} {F : X → ℝ} {h : ι → X → ℝ} namespace LMLExplore +/-- A sum of products of nonnegative and nonpositive reals is nonpositive. -/ +private lemma sum_mul_nonpos [Fintype ι] {c v : ι → ℝ} (hc : ∀ i, 0 ≤ c i) (hv : ∀ i, v i ≤ 0) : + ∑ i, c i * v i ≤ 0 := + Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (hc i) (hv i) + +/-- Products of nonnegative and nonpositive reals with a nonnegative sum all vanish. -/ +private lemma mul_eq_zero_of_sum_mul_nonneg [Fintype ι] {c v : ι → ℝ} (hc : ∀ i, 0 ≤ c i) + (hv : ∀ i, v i ≤ 0) (hs : 0 ≤ ∑ i, c i * v i) (i : ι) : c i * v i = 0 := + (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (hc i) (hv i)).1 + ((sum_mul_nonpos hc hv).antisymm hs) i (Finset.mem_univ _) + /-- The Lagrangian of a nonnegative multiplier is below the objective on the feasible set. -/ private lemma add_sum_mul_le [Fintype ι] (π : ι → ℝ≥0) {x : X} (hx : ∀ i, h i x ≤ 0) : F x + ∑ i, (π i : ℝ) * h i x ≤ F x := - add_le_of_nonpos_right <| Finset.sum_nonpos fun i _ ↦ - mul_nonpos_of_nonneg_of_nonpos (π i).2 (hx i) + add_le_of_nonpos_right <| sum_mul_nonpos (fun i ↦ (π i).2) hx /-- **Weak duality** in `EReal`: for every problem, the supremum over the multipliers of the infimum of the Lagrangian over `C` is below the infimum of the objective on the feasible set. -/ @@ -105,7 +115,7 @@ theorem iSup_iInf_add_le_iInf [Fintype ι] : Lagrangian `F y + ∑ i, π i * h i y` of some multiplier `π : ι → ℝ≥0`, with complementary slackness `π i * h i x = 0` for every `i`, then `x` minimizes `F` over `{y ∈ C | ∀ i, h i y ≤ 0}`. No convexity or constraint qualification is needed. -/ -theorem isMinOn_of_isMinOn_add_sum_mul [Fintype ι] {π : ι → ℝ≥0} {x : X} +theorem _root_.IsMinOn.of_add_sum_mul [Fintype ι] {π : ι → ℝ≥0} {x : X} (hmin : IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x) (hslack : ∀ i, (π i : ℝ) * h i x = 0) : IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x := by refine isMinOn_iff.2 fun y ⟨hy, hyh⟩ ↦ ?_ @@ -113,7 +123,6 @@ theorem isMinOn_of_isMinOn_add_sum_mul [Fintype ι] {π : ι → ℝ≥0} {x : X simp only [hslack, Finset.sum_const_zero, add_zero] at hle exact hle.trans (add_sum_mul_le π hyh) - /-- The objective (`none`) and the constraints (`some i`) of the program, as one family. -/ private def objConstr (F : X → ℝ) (h : ι → X → ℝ) (j : Option ι) (x : X) : ℝ := j.elim (F x) fun i ↦ h i x @@ -252,14 +261,10 @@ theorem exists_forall_le_add_sum_mul_of_convexLike [Fintype ι] -- `c (some i) * h i x₀ ≤ 0` would have a nonnegative sum, so every coefficient would vanish. have hc_pos : 0 < c none := by refine (hc_nonneg none).lt_of_ne' fun h0 ↦ hc ?_ - have hsum := hcx x₀ hx₀ - rw [h0, zero_mul, zero_mul, zero_add] at hsum - have hterm (i : ι) : c (some i) * h i x₀ ≤ 0 := - mul_nonpos_of_nonneg_of_nonpos (hc_nonneg _) (hx₀h i).le - have hzero (i : ι) : c (some i) = 0 := by - have := (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm i).1 - (le_antisymm (Finset.sum_nonpos fun i _ ↦ hterm i) hsum) i (Finset.mem_univ _) - exact (mul_eq_zero.1 this).resolve_right (hx₀h i).ne + have hsum : 0 ≤ ∑ i, c (some i) * h i x₀ := by simpa [h0] using hcx x₀ hx₀ + have hzero (i : ι) : c (some i) = 0 := + (mul_eq_zero.1 (mul_eq_zero_of_sum_mul_nonneg (fun _ ↦ hc_nonneg _) (fun i ↦ (hx₀h i).le) + hsum i)).resolve_right (hx₀h i).ne ext (_ | i) exacts [h0, hzero i] -- Normalize the coefficient of the objective to `1`. @@ -276,9 +281,12 @@ theorem exists_forall_le_add_sum_mul_of_convexLike [Fintype ι] exact hcx x hx exact ⟨fun i ↦ ⟨c (some i) / c none, div_nonneg (hc_nonneg _) hc_pos.le⟩, hL⟩ -/-- **Weak duality.** For every multiplier `π : ι → ℝ≥0`, the infimum over `C` of the Lagrangian -`F x + ∑ i, π i * h i x` is at most the infimum of `F` over the feasible set -`{x ∈ C | ∀ i, h i x ≤ 0}`. Values are in `EReal`, so no boundedness is assumed: when `F` is +/-- **Strong duality under Slater's condition with an attained dual optimum**, for convex-like +data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`, as in +`LMLExplore.exists_forall_le_add_sum_mul_of_convexLike`. If some `x₀ ∈ C` satisfies `h i x₀ < 0` for +every `i`, then some multiplier `π : ι → ℝ≥0` makes the infimum of `F` over the feasible set +`{x ∈ C | ∀ i, h i x ≤ 0}` equal to the infimum over `C` of the Lagrangian +`F x + ∑ i, π i * h i x`. Values are in `EReal`, so no boundedness is assumed: when `F` is unbounded below on the feasible set, both sides are `⊥`. -/ theorem exists_iInf_eq_iInf_add_of_convexLike [Fintype ι] (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → @@ -328,20 +336,16 @@ theorem isMinOn_iff_exists_isMinOn_add_sum_mul_of_convexLike [Fintype ι] IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x ↔ ∃ π : ι → ℝ≥0, IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x ∧ ∀ i, (π i : ℝ) * h i x = 0 := by - have hterm (π : ι → ℝ≥0) (y : X) (hyh : ∀ i, h i y ≤ 0) (i : ι) : (π i : ℝ) * h i y ≤ 0 := - mul_nonpos_of_nonneg_of_nonpos (π i).2 (hyh i) constructor · intro hmin obtain ⟨π, hπ⟩ := exists_forall_le_add_sum_mul_of_convexLike hconv hslater (m := F x) fun y hy hyh ↦ isMinOn_iff.1 hmin y ⟨hy, hyh⟩ -- At `x` the sum of the nonpositive terms `π i * h i x` is nonnegative, hence each is zero. - have hsum : ∑ i, (π i : ℝ) * h i x = 0 := - le_antisymm (Finset.sum_nonpos fun i _ ↦ hterm π x hxh i) (by linarith [hπ x hx]) - have hslack (i : ι) : (π i : ℝ) * h i x = 0 := - (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ hterm π x hxh i).1 hsum i (Finset.mem_univ _) - exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hsum] using hπ y hy, hslack⟩ + have hslack : ∀ i, (π i : ℝ) * h i x = 0 := + mul_eq_zero_of_sum_mul_nonneg (fun i ↦ (π i).2) hxh (by linarith [hπ x hx]) + exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hslack] using hπ y hy, hslack⟩ · rintro ⟨π, hmin, hslack⟩ - exact isMinOn_of_isMinOn_add_sum_mul hmin hslack + exact hmin.of_add_sum_mul hslack section ConvexOn From 1b6b1e6b8608e369bf1bb3ceacc8904aa1512180 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:50:47 +0100 Subject: [PATCH 6/6] refactor: name the joint convex-like condition and export the sum lemmas Introduce `LMLExplore.JointlyConvexLikeOn` with `jointlyConvexLikeOn_iff`, use it in the five convex-like duality theorems, and make its introduction from convexity public as `ConvexOn.jointlyConvexLikeOn`. Move the general sum lemmas to `LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean` as the public `Finset.sum_mul_nonpos` and `Finset.mul_eq_zero_of_sum_mul_nonneg`, and replace the private `combo_lt_combo` by Mathlib's `convex_Iio`. Co-Authored-By: Claude Code --- .../Order/BigOperators/Ring/Finset.lean | 44 ++++++++ .../Analysis/Convex/LagrangeDuality.lean | 105 +++++++++--------- 2 files changed, 97 insertions(+), 52 deletions(-) create mode 100644 LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean diff --git a/LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean b/LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean new file mode 100644 index 00000000..09f39f79 --- /dev/null +++ b/LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Algebra.Order.Ring.Defs + +/-! +# Sums of products of nonnegative and nonpositive terms + +A sum `∑ i ∈ s, c i * v i` with `0 ≤ c i` and `v i ≤ 0` for `i ∈ s` is nonpositive, so it is +nonnegative only when every product `c i * v i` vanishes. With `c` a vector of Lagrange multipliers +and `v` the values of the constraints at a feasible point, the second statement is complementary +slackness. + +## Main statements + +* `Finset.sum_mul_nonpos`: `∑ i ∈ s, c i * v i ≤ 0`. +* `Finset.mul_eq_zero_of_sum_mul_nonneg`: if moreover `0 ≤ ∑ i ∈ s, c i * v i`, then + `c i * v i = 0` for every `i ∈ s`. +-/ + +public section + +namespace Finset + +variable {ι R : Type*} [NonUnitalNonAssocSemiring R] [PartialOrder R] [IsOrderedAddMonoid R] + [PosMulMono R] {s : Finset ι} {c v : ι → R} + +/-- A sum of products of nonnegative and nonpositive terms is nonpositive. -/ +theorem sum_mul_nonpos (hc : ∀ i ∈ s, 0 ≤ c i) (hv : ∀ i ∈ s, v i ≤ 0) : + ∑ i ∈ s, c i * v i ≤ 0 := + sum_nonpos fun i hi ↦ mul_nonpos_of_nonneg_of_nonpos (hc i hi) (hv i hi) + +/-- Products of nonnegative and nonpositive terms with a nonnegative sum all vanish. -/ +theorem mul_eq_zero_of_sum_mul_nonneg (hc : ∀ i ∈ s, 0 ≤ c i) (hv : ∀ i ∈ s, v i ≤ 0) + (hs : 0 ≤ ∑ i ∈ s, c i * v i) {i : ι} (hi : i ∈ s) : c i * v i = 0 := + (sum_eq_zero_iff_of_nonpos fun i hi ↦ mul_nonpos_of_nonneg_of_nonpos (hc i hi) (hv i hi)).1 + ((sum_mul_nonpos hc hv).antisymm hs) i hi + +end Finset diff --git a/LMLExplore/Analysis/Convex/LagrangeDuality.lean b/LMLExplore/Analysis/Convex/LagrangeDuality.lean index 7253f568..0569589a 100644 --- a/LMLExplore/Analysis/Convex/LagrangeDuality.lean +++ b/LMLExplore/Analysis/Convex/LagrangeDuality.lean @@ -5,6 +5,7 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.Algebra.Order.BigOperators.Ring.Finset public import Mathlib.Analysis.LocallyConvex.Separation public import Mathlib.Data.EReal.Basic public import Mathlib.Basic.NNReal.Basic @@ -25,7 +26,8 @@ Theorem 1; §8.6, Theorem 1]. The existence of multipliers only needs `F` and `h` to be jointly *convex-like* on `C` in the sense of Fan [Fan53]: for `x, y ∈ C` and weights `a, b`, some `z ∈ C` has `F z` and every `h i z` below -the corresponding convex combinations of the values at `x` and `y`. It is stated in that form in +the corresponding convex combinations of the values at `x` and `y` +(`LMLExplore.JointlyConvexLikeOn`). It is stated in that form in `LMLExplore.exists_forall_le_add_sum_mul_of_convexLike`, which needs no linear structure on the domain and so applies to convex sets of probability measures, which carry no real scalar multiplication. Strong duality and the saddle point characterization are stated in the same @@ -40,6 +42,11 @@ This is the duality behind the dual formula of the minimal Kullback–Leibler di of laws defined by finitely many moment constraints, `KL_inf`, as the maximal expected logarithm of a bet `1 + ∑ i, π i * g i`. +## Main definitions + +* `LMLExplore.JointlyConvexLikeOn C F h`: `F` and the `h i` are jointly convex-like on `C`; + `ConvexOn.jointlyConvexLikeOn` derives it from convexity. + ## Main statements * `LMLExplore.iSup_iInf_add_le_iInf`: weak duality in `EReal`, with no hypothesis. @@ -87,21 +94,26 @@ variable {X ι : Type*} {C : Set X} {F : X → ℝ} {h : ι → X → ℝ} namespace LMLExplore -/-- A sum of products of nonnegative and nonpositive reals is nonpositive. -/ -private lemma sum_mul_nonpos [Fintype ι] {c v : ι → ℝ} (hc : ∀ i, 0 ≤ c i) (hv : ∀ i, v i ≤ 0) : - ∑ i, c i * v i ≤ 0 := - Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (hc i) (hv i) - -/-- Products of nonnegative and nonpositive reals with a nonnegative sum all vanish. -/ -private lemma mul_eq_zero_of_sum_mul_nonneg [Fintype ι] {c v : ι → ℝ} (hc : ∀ i, 0 ≤ c i) - (hv : ∀ i, v i ≤ 0) (hs : 0 ≤ ∑ i, c i * v i) (i : ι) : c i * v i = 0 := - (Finset.sum_eq_zero_iff_of_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (hc i) (hv i)).1 - ((sum_mul_nonpos hc hv).antisymm hs) i (Finset.mem_univ _) +/-- `F` and the family `h` are *jointly convex-like* on `C`, in the sense of Fan [Fan53]: for +`x, y ∈ C` and weights `a, b ≥ 0` with `a + b = 1`, some `z ∈ C` has `F z` and every `h i z` below +the corresponding convex combinations of the values at `x` and `y`. Convex functions on a convex +set are jointly convex-like (`ConvexOn.jointlyConvexLikeOn`). The definition needs no linear +structure on `X`, so it also applies to functionals of probability measures, taking `z` to be a +mixture. -/ +def JointlyConvexLikeOn (C : Set X) (F : X → ℝ) (h : ι → X → ℝ) : Prop := + ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y + +/-- The defining property of `LMLExplore.JointlyConvexLikeOn`. -/ +theorem jointlyConvexLikeOn_iff : JointlyConvexLikeOn C F h ↔ + ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → + ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y := + Iff.rfl /-- The Lagrangian of a nonnegative multiplier is below the objective on the feasible set. -/ private lemma add_sum_mul_le [Fintype ι] (π : ι → ℝ≥0) {x : X} (hx : ∀ i, h i x ≤ 0) : F x + ∑ i, (π i : ℝ) * h i x ≤ F x := - add_le_of_nonpos_right <| sum_mul_nonpos (fun i ↦ (π i).2) hx + add_le_of_nonpos_right <| Finset.sum_mul_nonpos (fun i _ ↦ (π i).2) fun i _ ↦ hx i /-- **Weak duality** in `EReal`: for every problem, the supremum over the multipliers of the infimum of the Lagrangian over `C` is below the infimum of the objective on the feasible set. -/ @@ -140,24 +152,18 @@ private lemma isOpen_strictEpigraph [Finite ι] : IsOpen (strictEpigraph C F h) exact isOpen_biUnion fun x _ ↦ isOpen_iInter_of_finite fun j ↦ isOpen_lt continuous_const (continuous_apply j) -/-- A convex combination of two strict inequalities is strict. -/ -private lemma combo_lt_combo {a b s t u w : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) - (hs : s < u) (ht : t < w) : a * s + b * t < a * u + b * w := by - rcases ha.eq_or_lt with rfl | ha - · obtain rfl : b = 1 := by linarith - linarith - · nlinarith [mul_lt_mul_of_pos_left hs ha, mul_le_mul_of_nonneg_left ht.le hb] - -private lemma convex_strictEpigraph - (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) : +private lemma convex_strictEpigraph (hconv : JointlyConvexLikeOn C F h) : Convex ℝ (strictEpigraph C F h) := by rintro v ⟨x, hx, hxv⟩ w ⟨y, hy, hyw⟩ a b ha hb hab - obtain ⟨z, hz, hFz, hhz⟩ := hconv x hx y hy a b ha hb hab + obtain ⟨z, hz, hFz, hhz⟩ := jointlyConvexLikeOn_iff.1 hconv x hx y hy a b ha hb hab refine ⟨z, hz, fun j ↦ ?_⟩ have hz' : objConstr F h j z ≤ a * objConstr F h j x + b * objConstr F h j y := by cases j <;> simp [objConstr, hFz, hhz] - simpa using hz'.trans_lt (combo_lt_combo ha hb hab (hxv j) (hyw j)) + -- The convex combination of `objConstr F h j x - v j < 0` and `objConstr F h j y - w j < 0`. + have hlt := convex_Iio (0 : ℝ) (sub_neg.2 (hxv j)) (sub_neg.2 (hyw j)) ha hb hab + simp only [mem_Iio, smul_eq_mul] at hlt + simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] + linarith private lemma mem_strictEpigraph_of_le {v w : Option ι → ℝ} (hv : v ∈ strictEpigraph C F h) (hvw : v ≤ w) : w ∈ strictEpigraph C F h := by @@ -203,8 +209,7 @@ constraints, has `c none * m ≤ c none * F x + ∑ i, c (some i) * h i x` for e Under Slater's condition `c none` is positive, which gives `LMLExplore.exists_forall_le_add_sum_mul_of_convexLike`. -/ theorem exists_ne_zero_forall_le_of_convexLike [Fintype ι] - (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hconv : JointlyConvexLikeOn C F h) {m : ℝ} (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : ∃ c : Option ι → ℝ, c ≠ 0 ∧ (∀ j, 0 ≤ c j) ∧ ∀ x ∈ C, c none * m ≤ c none * F x + ∑ i, c (some i) * h i x := by @@ -239,19 +244,18 @@ theorem exists_ne_zero_forall_le_of_convexLike [Fintype ι] simpa [hfc, objConstr, p] using apply_le_of_forall_lt hf hx /-- **Lagrange multipliers under Slater's condition** [Lue69, §8.3, Theorem 1], for convex-like -data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C`: for `x, y ∈ C` -and weights `a, b ≥ 0` with `a + b = 1`, some `z ∈ C` has `F z` and every `h i z` below the -corresponding convex combinations of the values at `x` and `y`. If some `x₀ ∈ C` satisfies -`h i x₀ < 0` for every `i` and `m` is a lower bound of `F` on the feasible set -`{x ∈ C | ∀ i, h i x ≤ 0}`, then some multiplier `π : ι → ℝ≥0` makes `m` a lower bound of the -Lagrangian `F x + ∑ i, π i * h i x` on all of `C`. +data [Fan53]. Let `F` and finitely many `h i` be jointly convex-like on a set `C` +(`LMLExplore.JointlyConvexLikeOn`): for `x, y ∈ C` and weights `a, b ≥ 0` with `a + b = 1`, some +`z ∈ C` has `F z` and every `h i z` below the corresponding convex combinations of the values at +`x` and `y`. If some `x₀ ∈ C` satisfies `h i x₀ < 0` for every `i` and `m` is a lower bound of +`F` on the feasible set `{x ∈ C | ∀ i, h i x ≤ 0}`, then some multiplier `π : ι → ℝ≥0` makes `m` a +lower bound of the Lagrangian `F x + ∑ i, π i * h i x` on all of `C`. No vector space structure on `X` is needed: this applies to convex sets of measures. For convex functions on a convex set, see `LMLExplore.exists_forall_le_add_sum_mul_of_slater`. -/ theorem exists_forall_le_add_sum_mul_of_convexLike [Fintype ι] - (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hconv : JointlyConvexLikeOn C F h) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {m : ℝ} (hm : ∀ x ∈ C, (∀ i, h i x ≤ 0) → m ≤ F x) : ∃ π : ι → ℝ≥0, ∀ x ∈ C, m ≤ F x + ∑ i, (π i : ℝ) * h i x := by @@ -263,8 +267,8 @@ theorem exists_forall_le_add_sum_mul_of_convexLike [Fintype ι] refine (hc_nonneg none).lt_of_ne' fun h0 ↦ hc ?_ have hsum : 0 ≤ ∑ i, c (some i) * h i x₀ := by simpa [h0] using hcx x₀ hx₀ have hzero (i : ι) : c (some i) = 0 := - (mul_eq_zero.1 (mul_eq_zero_of_sum_mul_nonneg (fun _ ↦ hc_nonneg _) (fun i ↦ (hx₀h i).le) - hsum i)).resolve_right (hx₀h i).ne + (mul_eq_zero.1 (Finset.mul_eq_zero_of_sum_mul_nonneg (fun _ _ ↦ hc_nonneg _) + (fun i _ ↦ (hx₀h i).le) hsum (Finset.mem_univ i))).resolve_right (hx₀h i).ne ext (_ | i) exacts [h0, hzero i] -- Normalize the coefficient of the objective to `1`. @@ -289,8 +293,7 @@ every `i`, then some multiplier `π : ι → ℝ≥0` makes the infimum of `F` o `F x + ∑ i, π i * h i x`. Values are in `EReal`, so no boundedness is assumed: when `F` is unbounded below on the feasible set, both sides are `⊥`. -/ theorem exists_iInf_eq_iInf_add_of_convexLike [Fintype ι] - (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hconv : JointlyConvexLikeOn C F h) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : ∃ π : ι → ℝ≥0, ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by @@ -315,8 +318,7 @@ every `i`, then the infimum of `F` over `{x ∈ C | ∀ i, h i x ≤ 0}` is the `π : ι → ℝ≥0` of the infimum over `C` of the Lagrangian `F x + ∑ i, π i * h i x`, in `EReal`. The supremum is attained (`LMLExplore.exists_iInf_eq_iInf_add_of_convexLike`). -/ theorem iInf_eq_iSup_iInf_add_of_convexLike [Fintype ι] - (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hconv : JointlyConvexLikeOn C F h) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = ⨆ π : ι → ℝ≥0, ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := by @@ -330,8 +332,7 @@ in `LMLExplore.exists_forall_le_add_sum_mul_of_convexLike`, with some `x₀ ∈ exactly when some multiplier `π : ι → ℝ≥0` makes `x` a minimizer over `C` of the Lagrangian `F y + ∑ i, π i * h i y`, with complementary slackness `π i * h i x = 0` for every `i`. -/ theorem isMinOn_iff_exists_isMinOn_add_sum_mul_of_convexLike [Fintype ι] - (hconv : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y) + (hconv : JointlyConvexLikeOn C F h) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {x : X} (hx : x ∈ C) (hxh : ∀ i, h i x ≤ 0) : IsMinOn F {y ∈ C | ∀ i, h i y ≤ 0} x ↔ ∃ π : ι → ℝ≥0, IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x ∧ @@ -341,8 +342,9 @@ theorem isMinOn_iff_exists_isMinOn_add_sum_mul_of_convexLike [Fintype ι] obtain ⟨π, hπ⟩ := exists_forall_le_add_sum_mul_of_convexLike hconv hslater (m := F x) fun y hy hyh ↦ isMinOn_iff.1 hmin y ⟨hy, hyh⟩ -- At `x` the sum of the nonpositive terms `π i * h i x` is nonnegative, hence each is zero. - have hslack : ∀ i, (π i : ℝ) * h i x = 0 := - mul_eq_zero_of_sum_mul_nonneg (fun i ↦ (π i).2) hxh (by linarith [hπ x hx]) + have hslack (i : ι) : (π i : ℝ) * h i x = 0 := + Finset.mul_eq_zero_of_sum_mul_nonneg (fun i _ ↦ (π i).2) (fun i _ ↦ hxh i) + ((le_add_iff_nonneg_right _).1 (hπ x hx)) (Finset.mem_univ i) exact ⟨π, isMinOn_iff.2 fun y hy ↦ by simpa [hslack] using hπ y hy, hslack⟩ · rintro ⟨π, hmin, hslack⟩ exact hmin.of_add_sum_mul hslack @@ -352,10 +354,9 @@ section ConvexOn variable [AddCommMonoid X] [SMul ℝ X] /-- Convex functions on a convex set are jointly convex-like there, witnessed by `a • x + b • y`. -/ -private lemma convexLike_of_convexOn (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) : - ∀ x ∈ C, ∀ y ∈ C, ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → a + b = 1 → - ∃ z ∈ C, F z ≤ a * F x + b * F y ∧ ∀ i, h i z ≤ a * h i x + b * h i y := - fun x hx y hy a b ha hb hab ↦ ⟨a • x + b • y, hF.1 hx hy ha hb hab, +theorem _root_.ConvexOn.jointlyConvexLikeOn (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) : + JointlyConvexLikeOn C F h := + jointlyConvexLikeOn_iff.2 fun x hx y hy a b ha hb hab ↦ ⟨a • x + b • y, hF.1 hx hy ha hb hab, by simpa using hF.2 hx hy ha hb hab, fun i ↦ by simpa using (hh i).2 hx hy ha hb hab⟩ variable [Fintype ι] @@ -369,7 +370,7 @@ theorem exists_forall_le_add_sum_mul_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, ConvexOn ℝ C (h i)) (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) {p : ℝ} (hp : ∀ x ∈ C, (∀ i, h i x ≤ 0) → p ≤ F x) : ∃ π : ι → ℝ≥0, ∀ x ∈ C, p ≤ F x + ∑ i, (π i : ℝ) * h i x := - exists_forall_le_add_sum_mul_of_convexLike (convexLike_of_convexOn hF hh) hslater hp + exists_forall_le_add_sum_mul_of_convexLike (hF.jointlyConvexLikeOn hh) hslater hp /-- **Strong duality under Slater's condition**, with an attained dual optimum. If `F` and the finitely many constraints `h i` are convex on `C`, some point of `C` satisfies every constraint @@ -403,7 +404,7 @@ theorem iInf_eq_iSup_iInf_add_of_slater (hF : ConvexOn ℝ C F) (hh : ∀ i, Con (hslater : ∃ x₀ ∈ C, ∀ i, h i x₀ < 0) : ⨅ x ∈ {x ∈ C | ∀ i, h i x ≤ 0}, (F x : EReal) = ⨆ π : ι → ℝ≥0, ⨅ x ∈ C, ((F x + ∑ i, (π i : ℝ) * h i x : ℝ) : EReal) := - iInf_eq_iSup_iInf_add_of_convexLike (convexLike_of_convexOn hF hh) hslater + iInf_eq_iSup_iInf_add_of_convexLike (hF.jointlyConvexLikeOn hh) hslater /-- **Complementary slackness under Slater's condition** [Lue69, §8.3, Theorem 1]. If `F` and the finitely many constraints `h i` are convex on `C`, some point of `C` satisfies every constraint @@ -417,7 +418,7 @@ theorem _root_.IsMinOn.exists_mul_eq_zero_and_isMinOn_add_sum_mul_of_slater {x : ∃ π : ι → ℝ≥0, (∀ i, (π i : ℝ) * h i x = 0) ∧ IsMinOn (fun y ↦ F y + ∑ i, (π i : ℝ) * h i y) C x := by obtain ⟨π, hπ, hslack⟩ := (isMinOn_iff_exists_isMinOn_add_sum_mul_of_convexLike - (convexLike_of_convexOn hF hh) hslater hx.1 hx.2).1 hmin + (hF.jointlyConvexLikeOn hh) hslater hx.1 hx.2).1 hmin exact ⟨π, hslack, hπ⟩ end ConvexOn