[RemyDegenne]

This PR extends the Lagrange duality file that #388 added to main, LMLExplore/Analysis/Convex/LagrangeDuality.lean. It covers the EValues Layer 1.4 Lagrange duality bullet, which belongs to Nulls generated by constraints and the dual formula for $\mathrm{KL}_{\inf}$. #388 states the theorems for ConvexOn ℝ functions on a vector space. This PR proves them for convex-like data in the sense of Fan [Fan53], on any type, and derives #388's ConvexOn statements from those versions.

Roadmap: EValues

Why the convex-like form is needed: the roadmap's consumer is the dual formula for $\mathrm{KL}_{\inf}$ (iInf_klDiv_constraintNull_eq in Suggested.lean), whose ≤ direction applies Lagrange duality "on the probability measures P with klDiv Q P < ∞ and the g i integrable". Probability measures have no real scalar multiplication, so ConvexOn ℝ cannot even be stated for them. klDiv Q · and the constraint integrals are, however, convex-like on mixtures. The theorems on main do not apply to this case.

Added (in LMLExplore unless stated):

• JointlyConvexLikeOn C F h: F and the h i are jointly convex-like on C [Fan53], with jointlyConvexLikeOn_iff unfolding it and ConvexOn.jointlyConvexLikeOn (root ConvexOn namespace) deriving it from convexity. The convex-like theorems below take it as hypothesis.
• exists_ne_zero_forall_le_of_convexLike: Fritz John multipliers for convex-like data, with no constraint qualification.
• exists_forall_le_add_sum_mul_of_convexLike: under Slater's condition, every lower bound of F on the feasible set is a lower bound of the Lagrangian on C for some π : ι → ℝ≥0, for convex-like data.
• exists_iInf_eq_iInf_add_of_convexLike: strong duality in EReal with an attained dual optimum, with no boundedness hypothesis (both sides are ⊥ when F is unbounded below on the feasible set).
• iInf_eq_iSup_iInf_add_of_convexLike: strong duality in EReal, for convex-like data.
• IsMinOn.of_add_sum_mul (root IsMinOn namespace, for dot notation on the Lagrangian-minimizer hypothesis): sufficiency of the saddle-point condition, with no hypothesis at all.
• isMinOn_iff_exists_isMinOn_add_sum_mul_of_convexLike: the saddle-point (KKT) characterization of minimizers, with complementary slackness.

Added in the new file LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean, as general infrastructure used by the duality proofs: Finset.sum_mul_nonpos (a sum of products of nonnegative and nonpositive terms is nonpositive) and Finset.mul_eq_zero_of_sum_mul_nonneg (such products with a nonnegative sum all vanish, i.e. complementary slackness). Neither exists in Mathlib at the pinned version.

Changed declarations from main, with the same names and statements: LMLExplore.exists_forall_le_add_sum_mul_of_slater, LMLExplore.exists_iInf_eq_iInf_add_of_slater, LMLExplore.iInf_eq_iSup_iInf_add_of_slater and IsMinOn.exists_mul_eq_zero_and_isMinOn_add_sum_mul_of_slater. They are now derived from the convex-like theorems. Their domain assumption is generalized from [AddCommGroup V] [Module ℝ V] to [AddCommMonoid X] [SMul ℝ X], the assumptions of ConvexOn itself. LMLExplore.iSup_iInf_add_le_iInf (weak duality) is unchanged and is used by the new proofs. The file keeps one separation argument, the convex-like one in Option ι → ℝ. #388's ConvexOn-specific private separation lemmas (isOpen_setOf_exists_lt, convex_setOf_exists_lt, exists_strongDual_le_of_slater) are removed because they duplicated it. LinearMap.prod_pi_apply_eq_sum_univ in LMLExplore/LinearAlgebra/Pi.lean stays on main untouched; this file no longer imports it.

Removed or renamed public declarations on main: none.

The proof separates (m, 0) from the open convex set of points of Option ι → ℝ that lie strictly above (F x, h · x) for some x ∈ C, using geometric_hahn_banach_open_point. This gives the Fritz John multipliers. Slater's condition then makes the coefficient of the objective nonzero.

I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for Lagrangian, Slater, KKT, Fritz John, duality and multiplier. Apart from #388's ConvexOn theorems, which this PR now derives, there is no Lagrange duality or KKT theorem. Mathlib's Analysis/Calculus/LagrangeMultipliers.lean covers the differentiable, equality-constrained local case. No Mathlib PR material is vendored. The informal sources, Luenberger, Fan, and Boyd–Vandenberghe (cited by #388), are cited in the file.

Local checks (not CI), at 1b6b1e6: scope: scoped: against 85118f1a081b539f64a455ca0dc7059bec5f4479; lake build passed (Build completed successfully (8569 jobs).); local-axioms: checked 2 changed module(s), 37 declaration(s); 0 violation(s); module-system, header-style and environment lint all passed.

🤖 Generated with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The convex-like Fritz John, Slater multiplier, EReal strong duality and saddle-point theorems state the intended results of [Lue69, Ch. 8] and [Fan53]. JointlyConvexLikeOn has a nontrivial witness (ConvexOn.jointlyConvexLikeOn) and consumers, and the edge cases (empty C, empty ι, a primal value of ⊥) are handled correctly.
✅	reuse	approved	claude/claude-opus-5-5	Neither Mathlib nor LMLExplore has a Lagrange duality, Slater, Fritz John or convex-like result, and the PR removes #388's duplicated ConvexOn separation argument so the ConvexOn theorems become one-line corollaries. The proof uses Mathlib's geometric_hahn_banach_open_point and LinearMap.pi_apply_eq_sum_univ, and the new Finset lemmas have no Mathlib counterpart.
✅	scope	approved	claude/claude-opus-5-5	Single-topic extension of #388's Lagrange duality file: the convex-like theorems are what the EValues KL_inf dual formula needs, since its ≤ direction applies duality on probability measures where ConvexOn cannot be stated (roadmap EValues/README.md:420-421). The ConvexOn theorems are re-derived from them, and the new Finset lemmas are infrastructure used directly by the proofs.
✅	attribution	approved	claude/claude-opus-5-5	The file cites its central informal sources inline: Luenberger [Lue69, §8.3, §8.4, §8.6] for the theorems and the separation proof, Fan [Fan53] for the convex-like hypothesis, and BV04 in the References; it names geometric_hahn_banach_open_point. No Mathlib PR or other formalization is copied, the new Finset lemmas are routine, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The convex-like Lagrange duality, Fritz John and saddle-point theorems are public, with JointlyConvexLikeOn hidden behind an _iff lemma and a constructor from ConvexOn; the ConvexOn forms keep their names as one-line specializations. The proof helpers are private and specific to this argument, the two general Finset lemmas sit at a path mirroring Mathlib's and do not duplicate it, and there is no compatibility surface.
✅	generality	approved	claude/claude-opus-5-5	Every result is proved for convex-like data on an arbitrary type, and the ConvexOn statements are one-line corollaries with the domain weakened to ConvexOn's own [AddCommMonoid X] [SMul ℝ X]. No assumption is unused or too strong, and the new Finset lemmas are stated for ordered semirings.
✅	placement	approved	claude/claude-opus-5-5	The new generic Finset.sum_mul_nonpos/Finset.mul_eq_zero_of_sum_mul_nonneg live in LMLExplore/Algebra/Order/BigOperators/Ring/Finset.lean, whose path matches the Mathlib module and which sits next to the existing Group/Finset.lean, and the convex-like duality material stays in LagrangeDuality.lean beside the ConvexOn versions derived from it. Dropping the LMLExplore.LinearAlgebra.Pi import is correct, and no import added by the diff is unused or overly broad.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in the file's existing stems with Fan's source term convexLike, _iff/_eq match genuine equivalences/equalities, and dot-notation declarations (IsMinOn.of_add_sum_mul, ConvexOn.jointlyConvexLikeOn, Finset.*) sit in the right namespaces with no Mathlib clashes. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new Finset file and the rewritten LagrangeDuality module docstring accurately describe their material, including the convex-like generalisation and the single real-valued exception. Every new or changed public declaration's docstring matches its statement and hypotheses, with no overclaiming or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are split into focused private lemmas (openness, convexity, upward closure, the two separating-functional bounds), carry comments at each non-obvious step, and use no change/show or undocumented defeq. The ConvexOn statements are now one-line derivations from the convex-like theorems, which removes the duplicated separation argument.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 1b6b1e6. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $4.45.}