oxilean_std/convex_optimization/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::Node;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8use super::types::{
9    BundleMethodSolver, CuttingPlaneSolver, FISTASolver, GeometricProgramSolver, GradientDescent,
10    L1NormFunction, MirrorDescentSolver, OnlineLearner, ProjectedGradient, ProximalGradientSolver,
11    QuadraticFunction, RipVerifier, SDPRelaxation, SinkhornSolver, ADMM,
12};
13
14pub fn app(f: Expr, a: Expr) -> Expr {
15    Expr::App(Node::new(f), Node::new(a))
16}
17pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
18    app(app(f, a), b)
19}
20pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
21    app(app2(f, a, b), c)
22}
23pub fn cst(s: &str) -> Expr {
24    Expr::Const(Name::str(s), vec![])
25}
26pub fn prop() -> Expr {
27    Expr::Sort(Level::zero())
28}
29pub fn type0() -> Expr {
30    Expr::Sort(Level::succ(Level::zero()))
31}
32pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
33    Expr::Pi(bi, Name::str(name), Node::new(dom), Node::new(body))
34}
35pub fn arrow(a: Expr, b: Expr) -> Expr {
36    pi(BinderInfo::Default, "_", a, b)
37}
38pub fn nat_ty() -> Expr {
39    cst("Nat")
40}
41pub fn real_ty() -> Expr {
42    cst("Real")
43}
44pub fn list_ty(elem: Expr) -> Expr {
45    app(cst("List"), elem)
46}
47pub fn fn_ty(dom: Expr, cod: Expr) -> Expr {
48    arrow(dom, cod)
49}
50/// `ConvexSet : (List Real -> Prop) -> Prop`
51/// Predicate asserting a set (represented as a characteristic function) is convex.
52pub fn convex_set_ty() -> Expr {
53    arrow(fn_ty(list_ty(real_ty()), prop()), prop())
54}
55/// `ConvexFunction : (List Real -> Real) -> Prop`
56/// Predicate asserting f: ℝ^n → ℝ is a convex function.
57pub fn convex_function_ty() -> Expr {
58    arrow(fn_ty(list_ty(real_ty()), real_ty()), prop())
59}
60/// `KktConditions : (List Real -> Real) -> List (List Real -> Real) -> List Real -> Prop`
61/// KKT optimality conditions for a constrained convex program.
62pub fn kkt_conditions_ty() -> Expr {
63    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
64    let list_rn_to_r = list_ty(rn_to_r.clone());
65    arrow(
66        rn_to_r,
67        arrow(list_rn_to_r, arrow(list_ty(real_ty()), prop())),
68    )
69}
70/// `Lagrangian : (List Real -> Real) -> List (List Real -> Real) -> List Real -> List Real -> Real`
71/// Lagrangian function L(x, λ) = f(x) + Σ λ_i g_i(x).
72pub fn lagrangian_ty() -> Expr {
73    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
74    let list_rn_to_r = list_ty(rn_to_r.clone());
75    arrow(
76        rn_to_r,
77        arrow(
78            list_rn_to_r,
79            arrow(list_ty(real_ty()), arrow(list_ty(real_ty()), real_ty())),
80        ),
81    )
82}
83/// `StrongDuality : Prop`
84/// Slater's condition implies strong duality: primal optimal = dual optimal.
85pub fn strong_duality_ty() -> Expr {
86    prop()
87}
88/// `ProjectionTheorem : Prop`
89/// Every nonempty closed convex set has a unique nearest point (projection).
90pub fn projection_theorem_ty() -> Expr {
91    prop()
92}
93/// `SupportingHyperplane : Prop`
94/// At every boundary point of a convex set there exists a supporting hyperplane.
95pub fn supporting_hyperplane_ty() -> Expr {
96    prop()
97}
98/// `JensenInequality : (List Real -> Real) -> Prop`
99/// For convex f: f(E\[X\]) ≤ E[f(X)].
100pub fn jensen_inequality_ty() -> Expr {
101    arrow(fn_ty(list_ty(real_ty()), real_ty()), prop())
102}
103/// `SlaterCondition : Prop`
104/// Strong duality holds for convex programs satisfying Slater's condition.
105pub fn slater_condition_ty() -> Expr {
106    prop()
107}
108/// `FenchelConjugate : (List Real -> Real) -> List Real -> Real`
109/// The Fenchel conjugate f*(y) = sup_x { <y,x> - f(x) }.
110pub fn fenchel_conjugate_ty() -> Expr {
111    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
112    arrow(rn_to_r, fn_ty(list_ty(real_ty()), real_ty()))
113}
114/// `FenchelRockafellarDuality : Prop`
115/// inf f(x) + g(Ax) = -inf f*(-A^T y) + g*(y) under qualification.
116pub fn fenchel_rockafellar_duality_ty() -> Expr {
117    prop()
118}
119/// `ConjugateSubgradient : (List Real -> Real) -> List Real -> List Real -> Prop`
120/// y ∈ ∂f*(x*) iff x* ∈ ∂f(y) (Fenchel–Young equality condition).
121pub fn conjugate_subgradient_ty() -> Expr {
122    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
123    let lr = list_ty(real_ty());
124    arrow(rn_to_r, arrow(lr.clone(), arrow(lr, prop())))
125}
126/// `LagrangianDualFunction : (List Real -> Real) -> List (List Real -> Real) -> List Real -> Real`
127/// Dual function q(λ) = inf_x L(x, λ).
128pub fn lagrangian_dual_function_ty() -> Expr {
129    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
130    let list_rn_to_r = list_ty(rn_to_r.clone());
131    arrow(
132        rn_to_r,
133        arrow(list_rn_to_r, fn_ty(list_ty(real_ty()), real_ty())),
134    )
135}
136/// `LinearIndependenceConstraintQualification : Prop`
137/// LICQ: gradients of active constraints are linearly independent at x*.
138pub fn licq_ty() -> Expr {
139    prop()
140}
141/// `MangasarianFromovitzCQ : Prop`
142/// MFCQ constraint qualification weaker than LICQ.
143pub fn mfcq_ty() -> Expr {
144    prop()
145}
146/// `ComplementarySlackness : List Real -> List Real -> Prop`
147/// λ_i g_i(x) = 0 for all i (complementary slackness conditions).
148pub fn complementary_slackness_ty() -> Expr {
149    let lr = list_ty(real_ty());
150    arrow(lr.clone(), arrow(lr, prop()))
151}
152/// `KktSufficiency : Prop`
153/// Under convexity, KKT conditions are sufficient for global optimality.
154pub fn kkt_sufficiency_ty() -> Expr {
155    prop()
156}
157/// `BarrierFunction : (List Real -> Prop) -> (List Real -> Real) -> Prop`
158/// A barrier function for a convex set: diverges at boundary.
159pub fn barrier_function_ty() -> Expr {
160    let rn_to_prop = fn_ty(list_ty(real_ty()), prop());
161    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
162    arrow(rn_to_prop, arrow(rn_to_r, prop()))
163}
164/// `PathFollowingMethod : Prop`
165/// Central path: x*(t) minimizes t·f(x) + φ(x) for barrier φ.
166pub fn path_following_method_ty() -> Expr {
167    prop()
168}
169/// `PredictorCorrectorMethod : Prop`
170/// Mehrotra predictor-corrector interior point algorithm converges in O(√n·L) steps.
171pub fn predictor_corrector_method_ty() -> Expr {
172    prop()
173}
174/// `CentralPathConvergence : Real -> Prop`
175/// The central path converges to the primal-dual optimal as t → ∞.
176pub fn central_path_convergence_ty() -> Expr {
177    arrow(real_ty(), prop())
178}
179/// `PositiveSemidefinite : List (List Real) -> Prop`
180/// Predicate that a matrix (as list of rows) is positive semidefinite.
181pub fn positive_semidefinite_ty() -> Expr {
182    let mat = list_ty(list_ty(real_ty()));
183    arrow(mat, prop())
184}
185/// `SdpFeasibility : List (List (List Real)) -> List Real -> Prop`
186/// SDP feasibility: ∑ x_i A_i ⪰ 0 for given data matrices {A_i}.
187pub fn sdp_feasibility_ty() -> Expr {
188    let mat = list_ty(list_ty(real_ty()));
189    let mats = list_ty(mat);
190    let lr = list_ty(real_ty());
191    arrow(mats, arrow(lr, prop()))
192}
193/// `SdpDuality : Prop`
194/// SDP strong duality under Slater's condition (Alaoglu–Fan theorem).
195pub fn sdp_duality_ty() -> Expr {
196    prop()
197}
198/// `SdpOptimality : List (List (List Real)) -> List Real -> List Real -> Real -> Prop`
199/// SDP optimality certificate: primal X and dual y satisfy complementarity.
200pub fn sdp_optimality_ty() -> Expr {
201    let mat = list_ty(list_ty(real_ty()));
202    let mats = list_ty(mat);
203    let lr = list_ty(real_ty());
204    arrow(mats, arrow(lr.clone(), arrow(lr, arrow(real_ty(), prop()))))
205}
206/// `SecondOrderCone : List Real -> Real -> Prop`
207/// (x, t) ∈ SOC iff ‖x‖ ≤ t.
208pub fn second_order_cone_ty() -> Expr {
209    let lr = list_ty(real_ty());
210    arrow(lr, arrow(real_ty(), prop()))
211}
212/// `SocpFeasibility : Prop`
213/// SOCP feasibility: minimize c^T x subject to second-order cone constraints.
214pub fn socp_feasibility_ty() -> Expr {
215    prop()
216}
217/// `Monomial : List Real -> List Real -> Real -> Real`
218/// Monomial c · ∏ x_i^{a_i} in geometric programming.
219pub fn monomial_ty() -> Expr {
220    let lr = list_ty(real_ty());
221    arrow(lr.clone(), arrow(lr, arrow(real_ty(), real_ty())))
222}
223/// `Posynomial : List (List Real -> Real) -> List Real -> Real`
224/// Posynomial: sum of monomials evaluated at x.
225pub fn posynomial_ty() -> Expr {
226    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
227    let lr = list_ty(real_ty());
228    arrow(list_ty(rn_to_r), arrow(lr, real_ty()))
229}
230/// `GeometricProgramDuality : Prop`
231/// GP can be converted to convex form via log transformation.
232pub fn geometric_program_duality_ty() -> Expr {
233    prop()
234}
235/// `SmoothGradientConvergence : Real -> Real -> Nat -> Prop`
236/// GD with step 1/L: f(x_k) - f* ≤ L‖x_0-x*‖²/(2k) for L-smooth f.
237pub fn smooth_gradient_convergence_ty() -> Expr {
238    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
239}
240/// `StronglyConvexConvergence : Real -> Real -> Nat -> Prop`
241/// GD converges linearly for μ-strongly convex L-smooth functions.
242pub fn strongly_convex_convergence_ty() -> Expr {
243    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
244}
245/// `ProximalOperator : (List Real -> Real) -> Real -> List Real -> List Real`
246/// prox_{t·f}(v) = argmin_x { f(x) + 1/(2t) ‖x - v‖² }.
247pub fn proximal_operator_ty() -> Expr {
248    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
249    let lr = list_ty(real_ty());
250    arrow(rn_to_r, arrow(real_ty(), fn_ty(lr.clone(), lr)))
251}
252/// `IstaConvergence : Real -> Real -> Nat -> Prop`
253/// ISTA (proximal gradient): f(x_k) - f* ≤ ‖x_0-x*‖²/(2tk).
254pub fn ista_convergence_ty() -> Expr {
255    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
256}
257/// `FistaConvergence : Real -> Nat -> Prop`
258/// FISTA (accelerated proximal gradient): O(1/k²) convergence rate.
259pub fn fista_convergence_ty() -> Expr {
260    arrow(real_ty(), arrow(nat_ty(), prop()))
261}
262/// `ProximalGradientDescent : (List Real -> Real) -> (List Real -> Real) -> Prop`
263/// Proximal gradient: minimize f(x) + g(x), f smooth, g proxable.
264pub fn proximal_gradient_descent_ty() -> Expr {
265    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
266    arrow(rn_to_r.clone(), arrow(rn_to_r, prop()))
267}
268/// `DouglasRachfordSplitting : Prop`
269/// DR splitting converges for sum of two maximal monotone operators.
270pub fn douglas_rachford_splitting_ty() -> Expr {
271    prop()
272}
273/// `ChambollePockAlgorithm : Real -> Real -> Nat -> Prop`
274/// Chambolle-Pock primal-dual algorithm with step sizes τ, σ satisfying τσ‖K‖² < 1.
275pub fn chambolle_pock_ty() -> Expr {
276    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
277}
278/// `AugmentedLagrangian : (List Real -> Real) -> List (List Real -> Real) -> Real -> List Real -> List Real -> Real`
279/// L_ρ(x, λ) = f(x) + λ^T h(x) + (ρ/2)‖h(x)‖².
280pub fn augmented_lagrangian_ty() -> Expr {
281    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
282    let list_rn_to_r = list_ty(rn_to_r.clone());
283    arrow(
284        rn_to_r,
285        arrow(
286            list_rn_to_r,
287            arrow(
288                real_ty(),
289                arrow(list_ty(real_ty()), arrow(list_ty(real_ty()), real_ty())),
290            ),
291        ),
292    )
293}
294/// `AdmmConvergence : Real -> Prop`
295/// ADMM converges to optimal for convex problems with penalty ρ > 0.
296pub fn admm_convergence_ty() -> Expr {
297    arrow(real_ty(), prop())
298}
299/// `SupportingHyperplaneCut : (List Real -> Real) -> List Real -> List Real -> Real -> Prop`
300/// At x_k: f(x) ≥ f(x_k) + g_k^T (x - x_k) for subgradient g_k.
301pub fn supporting_hyperplane_cut_ty() -> Expr {
302    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
303    let lr = list_ty(real_ty());
304    arrow(
305        rn_to_r,
306        arrow(lr.clone(), arrow(lr, arrow(real_ty(), prop()))),
307    )
308}
309/// `KelleyMethod : Prop`
310/// Kelley's cutting-plane method converges for convex Lipschitz functions.
311pub fn kelley_method_ty() -> Expr {
312    prop()
313}
314/// `BundleMethodConvergence : Real -> Prop`
315/// Bundle method for nonsmooth optimization converges with tolerance ε.
316pub fn bundle_method_convergence_ty() -> Expr {
317    arrow(real_ty(), prop())
318}
319/// `EllipsoidMethodComplexity : Real -> Real -> Nat -> Prop`
320/// Ellipsoid method finds ε-optimal solution in O(n² log(R/ε)) iterations.
321pub fn ellipsoid_method_complexity_ty() -> Expr {
322    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
323}
324/// `CenterOfGravityMethod : Nat -> Prop`
325/// Center-of-gravity method reduces feasible set volume by (1-1/n) per step.
326pub fn center_of_gravity_method_ty() -> Expr {
327    arrow(nat_ty(), prop())
328}
329/// `SubgradientInequality : (List Real -> Real) -> List Real -> List Real -> Prop`
330/// g ∈ ∂f(x): f(y) ≥ f(x) + g^T (y - x) for all y.
331pub fn subgradient_inequality_ty() -> Expr {
332    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
333    let lr = list_ty(real_ty());
334    arrow(rn_to_r, arrow(lr.clone(), arrow(lr, prop())))
335}
336/// `SubgradientMethodConvergence : Real -> Real -> Nat -> Prop`
337/// Subgradient method with step t_k = R/(G√k): best f - f* ≤ RG/√k.
338pub fn subgradient_method_convergence_ty() -> Expr {
339    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
340}
341/// `PolyakStepsize : Real -> Real -> Prop`
342/// Polyak step size t_k = (f(x_k) - f*)/(‖g_k‖²) gives optimal convergence.
343pub fn polyak_stepsize_ty() -> Expr {
344    arrow(real_ty(), arrow(real_ty(), prop()))
345}
346/// `StochasticGradientDescent : Real -> Nat -> Prop`
347/// SGD with step η: E[f(x_k)] - f* = O(σ/(μ√k)) for strongly convex f.
348pub fn sgd_convergence_ty() -> Expr {
349    arrow(real_ty(), arrow(nat_ty(), prop()))
350}
351/// `SvrgConvergence : Real -> Real -> Nat -> Prop`
352/// SVRG: variance-reduced SGD with geometric convergence rate (1 - μη/2)^k.
353pub fn svrg_convergence_ty() -> Expr {
354    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
355}
356/// `SarahConvergence : Real -> Real -> Nat -> Prop`
357/// SARAH: stochastic recursive gradient with near-optimal convergence.
358pub fn sarah_convergence_ty() -> Expr {
359    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
360}
361/// `SpiderConvergence : Real -> Real -> Nat -> Prop`
362/// SPIDER: stochastic path-integrated differential estimator convergence.
363pub fn spider_convergence_ty() -> Expr {
364    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
365}
366/// `DcpAtomConvex : (List Real -> Real) -> Prop`
367/// An atom is declared convex in the DCP ruleset.
368pub fn dcp_atom_convex_ty() -> Expr {
369    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
370    arrow(rn_to_r, prop())
371}
372/// `DcpCompositionRule : Prop`
373/// DCP composition rules: convex nondecreasing ∘ convex = convex, etc.
374pub fn dcp_composition_rule_ty() -> Expr {
375    prop()
376}
377/// `DcpVerification : (List Real -> Real) -> Prop`
378/// An expression satisfies DCP rules and is thus provably convex.
379pub fn dcp_verification_ty() -> Expr {
380    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
381    arrow(rn_to_r, prop())
382}
383/// `SelfConcordantBarrier : (List Real -> Real) -> Real -> Prop`
384/// A function phi is nu-self-concordant: |D^3 phi(x)\[h,h,h\]| <= 2(D^2 phi(x)\[h,h\])^{3/2}.
385pub fn self_concordant_barrier_ty() -> Expr {
386    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
387    arrow(rn_to_r, arrow(real_ty(), prop()))
388}
389/// `SelfConcordantComplexity : Real -> Nat -> Prop`
390/// IPM with nu-self-concordant barrier terminates in O(sqrt(nu) * log(1/eps)) Newton steps.
391pub fn self_concordant_complexity_ty() -> Expr {
392    arrow(real_ty(), arrow(nat_ty(), prop()))
393}
394/// `LogarithmicBarrier : Nat -> (List Real -> Real) -> Prop`
395/// The logarithmic barrier -sum log(-g_i(x)) is self-concordant with parameter m.
396pub fn logarithmic_barrier_ty() -> Expr {
397    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
398    arrow(nat_ty(), arrow(rn_to_r, prop()))
399}
400/// `NewtonDecrement : (List Real -> Real) -> List Real -> Real`
401/// lambda(f,x)^2 = grad f(x)^T \[Hess f(x)\]^{-1} grad f(x), the Newton decrement squared.
402pub fn newton_decrement_ty() -> Expr {
403    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
404    let lr = list_ty(real_ty());
405    arrow(rn_to_r, arrow(lr, real_ty()))
406}
407/// `SdpSlaterCondition : Prop`
408/// SDP Slater: there exists strictly feasible X > 0 satisfying primal constraints.
409pub fn sdp_slater_condition_ty() -> Expr {
410    prop()
411}
412/// `SdpComplementarity : List (List Real) -> List (List Real) -> Prop`
413/// SDP complementarity: X >= 0, S >= 0, and XS = 0 at optimality.
414pub fn sdp_complementarity_ty() -> Expr {
415    let mat = list_ty(list_ty(real_ty()));
416    arrow(mat.clone(), arrow(mat, prop()))
417}
418/// `SdpDualityGap : List (List Real) -> List Real -> Real`
419/// Duality gap = tr(C X) - b^T y for primal X, dual y.
420pub fn sdp_duality_gap_ty() -> Expr {
421    let mat = list_ty(list_ty(real_ty()));
422    let lr = list_ty(real_ty());
423    arrow(mat, arrow(lr, real_ty()))
424}
425/// `LorentzCone : Nat -> Prop`
426/// The Lorentz (ice cream) cone L^n = {(x,t) : ||x|| <= t} in R^{n+1}.
427pub fn lorentz_cone_ty() -> Expr {
428    arrow(nat_ty(), prop())
429}
430/// `SocpDuality : Prop`
431/// SOCP strong duality: primal optimal = dual optimal under Slater's condition.
432pub fn socp_duality_ty() -> Expr {
433    prop()
434}
435/// `RotatedLorentzCone : List Real -> Real -> Real -> Prop`
436/// Rotated Lorentz cone: (x,y,z) with ||x||^2 <= 2yz, y,z >= 0.
437pub fn rotated_lorentz_cone_ty() -> Expr {
438    let lr = list_ty(real_ty());
439    arrow(lr, arrow(real_ty(), arrow(real_ty(), prop())))
440}
441/// `AdmmLinearConvergence : Real -> Real -> Nat -> Prop`
442/// ADMM with penalty rho converges linearly: ||x^k - x*|| <= C * r^k.
443pub fn admm_linear_convergence_ty() -> Expr {
444    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
445}
446/// `AdmmPrimalResidual : List Real -> List Real -> Real -> Prop`
447/// Primal residual ||Ax + Bz - c|| <= eps_pri at iteration k.
448pub fn admm_primal_residual_ty() -> Expr {
449    let lr = list_ty(real_ty());
450    arrow(lr.clone(), arrow(lr, arrow(real_ty(), prop())))
451}
452/// `AdmmDualResidual : List Real -> Real -> Prop`
453/// Dual residual rho * ||B^T(z^k - z^{k-1})|| <= eps_dual.
454pub fn admm_dual_residual_ty() -> Expr {
455    let lr = list_ty(real_ty());
456    arrow(lr, arrow(real_ty(), prop()))
457}
458/// `ProximalPointAlgorithm : (List Real -> Real) -> Real -> Nat -> Prop`
459/// PPA: x^{k+1} = prox_{t f}(x^k) converges to argmin f.
460pub fn proximal_point_algorithm_ty() -> Expr {
461    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
462    arrow(rn_to_r, arrow(real_ty(), arrow(nat_ty(), prop())))
463}
464/// `ResolventOperator : (List Real -> List Real -> Prop) -> Real -> List Real -> List Real`
465/// Resolvent J_{t A}(x) = (I + tA)^{-1}(x) of a monotone operator A.
466pub fn resolvent_operator_ty() -> Expr {
467    let rn_rn_prop = fn_ty(list_ty(real_ty()), fn_ty(list_ty(real_ty()), prop()));
468    let lr = list_ty(real_ty());
469    arrow(rn_rn_prop, arrow(real_ty(), fn_ty(lr.clone(), lr)))
470}
471/// `FirmlyNonexpansive : (List Real -> List Real) -> Prop`
472/// T is firmly nonexpansive: ||Tx - Ty||^2 <= <Tx - Ty, x - y>.
473pub fn firmly_nonexpansive_ty() -> Expr {
474    let lr = list_ty(real_ty());
475    let rn_to_rn = fn_ty(lr.clone(), lr);
476    arrow(rn_to_rn, prop())
477}
478/// `BregmanDivergence : (List Real -> Real) -> List Real -> List Real -> Real`
479/// D_h(x,y) = h(x) - h(y) - <grad h(y), x-y> for strictly convex h.
480pub fn bregman_divergence_ty() -> Expr {
481    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
482    let lr = list_ty(real_ty());
483    arrow(rn_to_r, arrow(lr.clone(), arrow(lr, real_ty())))
484}
485/// `MirrorDescentConvergence : Real -> Real -> Nat -> Prop`
486/// Mirror descent: sum_{t=1}^{T} f(x_t) - f(x*) <= D_h(x*,x_1)/eta + eta*sum||grad f||^2_*.
487pub fn mirror_descent_convergence_ty() -> Expr {
488    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
489}
490/// `NegativeEntropyFunction : List Real -> Real`
491/// Negative entropy: h(x) = sum x_i log(x_i), used as Bregman generating function.
492pub fn negative_entropy_function_ty() -> Expr {
493    let lr = list_ty(real_ty());
494    fn_ty(lr, real_ty())
495}
496/// `ExponentialWeightsAlgorithm : Real -> Nat -> Prop`
497/// EWA/Hedge: mirror descent with negative entropy achieves O(sqrt(T log n)) regret.
498pub fn exponential_weights_algorithm_ty() -> Expr {
499    arrow(real_ty(), arrow(nat_ty(), prop()))
500}
501/// `SagaConvergence : Real -> Real -> Nat -> Prop`
502/// SAGA: variance-reduced SGD with O(1/k) convergence for non-strongly-convex.
503pub fn saga_convergence_ty() -> Expr {
504    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
505}
506/// `AdamConvergence : Real -> Real -> Real -> Nat -> Prop`
507/// Adam optimizer: adaptive moment estimation with O(1/sqrt(T)) regret bound.
508pub fn adam_convergence_ty() -> Expr {
509    arrow(
510        real_ty(),
511        arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop()))),
512    )
513}
514/// `MomentumSgd : Real -> Real -> Nat -> Prop`
515/// SGD with momentum (heavy ball): beta-momentum improves convergence constant.
516pub fn momentum_sgd_ty() -> Expr {
517    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
518}
519/// `MaximalMonotoneOperator : (List Real -> List (List Real)) -> Prop`
520/// A set-valued operator A: R^n -> 2^{R^n} is maximal monotone.
521pub fn maximal_monotone_operator_ty() -> Expr {
522    let lr = list_ty(real_ty());
523    let set_valued = fn_ty(lr.clone(), list_ty(lr));
524    arrow(set_valued, prop())
525}
526/// `MonotoneInclusionProblem : (List Real -> List (List Real)) -> List Real -> Prop`
527/// Find x* such that 0 in A(x*) for maximal monotone operator A.
528pub fn monotone_inclusion_problem_ty() -> Expr {
529    let lr = list_ty(real_ty());
530    let set_valued = fn_ty(lr.clone(), list_ty(lr.clone()));
531    arrow(set_valued, arrow(lr, prop()))
532}
533/// `SplittingConvergence : Prop`
534/// Operator splitting methods (DR, FBS, etc.) converge for sum of monotone operators.
535pub fn splitting_convergence_ty() -> Expr {
536    prop()
537}
538/// `KantorovichProblem : (List Real -> List Real -> Real) -> List Real -> List Real -> Real`
539/// Kantorovich: min_{gamma in Pi(mu,nu)} integral c(x,y) d_gamma(x,y) over transport plans.
540pub fn kantorovich_problem_ty() -> Expr {
541    let lr = list_ty(real_ty());
542    let cost = fn_ty(lr.clone(), fn_ty(lr.clone(), real_ty()));
543    arrow(cost, arrow(lr.clone(), arrow(lr, real_ty())))
544}
545/// `KantorovichDuality : Prop`
546/// min_{gamma} integral c d_gamma = max_{phi,psi: phi(x)+psi(y)<=c(x,y)} integral phi d_mu + integral psi d_nu.
547pub fn kantorovich_duality_ty() -> Expr {
548    prop()
549}
550/// `WassersteinDistance : Real -> List Real -> List Real -> Real`
551/// W_p(mu,nu) = (min_{gamma in Pi(mu,nu)} integral ||x-y||^p d_gamma)^{1/p}.
552pub fn wasserstein_distance_ty() -> Expr {
553    let lr = list_ty(real_ty());
554    arrow(real_ty(), arrow(lr.clone(), arrow(lr, real_ty())))
555}
556/// `SinkhornAlgorithm : Real -> Nat -> Prop`
557/// Sinkhorn: entropic regularization gives O(n^2/eps^2) algorithm for OT.
558pub fn sinkhorn_algorithm_ty() -> Expr {
559    arrow(real_ty(), arrow(nat_ty(), prop()))
560}
561/// `RestrictedIsometryProperty : Nat -> Real -> List (List Real) -> Prop`
562/// RIP-s: (1-delta)||x||^2 <= ||Ax||^2 <= (1+delta)||x||^2 for all s-sparse x.
563pub fn restricted_isometry_property_ty() -> Expr {
564    let mat = list_ty(list_ty(real_ty()));
565    arrow(nat_ty(), arrow(real_ty(), arrow(mat, prop())))
566}
567/// `BasisPursuitRecovery : List (List Real) -> List Real -> Nat -> Prop`
568/// If A satisfies RIP-{2s}, basis pursuit recovers s-sparse x from Ax = b.
569pub fn basis_pursuit_recovery_ty() -> Expr {
570    let mat = list_ty(list_ty(real_ty()));
571    let lr = list_ty(real_ty());
572    arrow(mat, arrow(lr, arrow(nat_ty(), prop())))
573}
574/// `LassoSparsity : Real -> Nat -> Prop`
575/// LASSO with appropriate lambda recovers s-sparse signal with O(s log p / n) samples.
576pub fn lasso_sparsity_ty() -> Expr {
577    arrow(real_ty(), arrow(nat_ty(), prop()))
578}
579/// `NuclearNorm : List (List Real) -> Real`
580/// ||X||_* = sum sigma_i(X), the nuclear norm (sum of singular values).
581pub fn nuclear_norm_ty() -> Expr {
582    let mat = list_ty(list_ty(real_ty()));
583    fn_ty(mat, real_ty())
584}
585/// `MatrixCompletionTheorem : Nat -> Nat -> Nat -> Real -> Prop`
586/// If rank-r matrix M satisfies incoherence, nuclear norm minimization recovers M
587/// from O(r n log n) entries.
588pub fn matrix_completion_theorem_ty() -> Expr {
589    arrow(
590        nat_ty(),
591        arrow(nat_ty(), arrow(nat_ty(), arrow(real_ty(), prop()))),
592    )
593}
594/// `RobustPca : List (List Real) -> List (List Real) -> List (List Real) -> Prop`
595/// Robust PCA: decompose M = L + S, L low-rank, S sparse, via PCP convex program.
596pub fn robust_pca_ty() -> Expr {
597    let mat = list_ty(list_ty(real_ty()));
598    arrow(mat.clone(), arrow(mat.clone(), arrow(mat, prop())))
599}
600/// `ChanceConstraint : (List Real -> Prop) -> Real -> Prop`
601/// P(g(x) <= 0) >= 1 - eps: probabilistic constraint with confidence 1-eps.
602pub fn chance_constraint_ty() -> Expr {
603    let rn_prop = fn_ty(list_ty(real_ty()), prop());
604    arrow(rn_prop, arrow(real_ty(), prop()))
605}
606/// `DistributionallyRobustObjective : (List Real -> Real) -> Real -> Prop`
607/// DRO: min_x max_{P in U} E_P\[f(x,xi)\] over ambiguity set U.
608pub fn distributionally_robust_objective_ty() -> Expr {
609    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
610    arrow(rn_to_r, arrow(real_ty(), prop()))
611}
612/// `WassersteinAmbiguitySet : List Real -> Real -> Prop`
613/// Wasserstein ball of radius rho around empirical distribution P_N.
614pub fn wasserstein_ambiguity_set_ty() -> Expr {
615    let lr = list_ty(real_ty());
616    arrow(lr, arrow(real_ty(), prop()))
617}
618/// `CvarConstraint : (List Real -> Real) -> Real -> Real -> Prop`
619/// Conditional value-at-risk CVaR_alpha(f(x,xi)) <= t is a convex constraint in x, t.
620pub fn cvar_constraint_ty() -> Expr {
621    let rn_to_r = fn_ty(list_ty(real_ty()), real_ty());
622    arrow(rn_to_r, arrow(real_ty(), arrow(real_ty(), prop())))
623}
624/// `OnlineConvexOptimization : Nat -> Real -> Prop`
625/// OCO regret bound: sum_{t=1}^T f_t(x_t) - min_x sum f_t(x) <= R_T.
626pub fn online_convex_optimization_ty() -> Expr {
627    arrow(nat_ty(), arrow(real_ty(), prop()))
628}
629/// `FtrlRegretBound : Real -> Nat -> Prop`
630/// FTRL achieves O(sqrt(T)) regret for convex losses with regularizer.
631pub fn ftrl_regret_bound_ty() -> Expr {
632    arrow(real_ty(), arrow(nat_ty(), prop()))
633}
634/// `AdaptiveRegretBound : Real -> Real -> Nat -> Prop`
635/// Adaptive online algorithms achieve tighter regret via local norms.
636pub fn adaptive_regret_bound_ty() -> Expr {
637    arrow(real_ty(), arrow(real_ty(), arrow(nat_ty(), prop())))
638}
639/// `OnlineGradientDescentRegret : Real -> Nat -> Prop`
640/// OGD regret: O(G*R*sqrt(T)) where G is gradient bound, R is domain diameter.
641pub fn online_gradient_descent_regret_ty() -> Expr {
642    arrow(real_ty(), arrow(nat_ty(), prop()))
643}
644/// Build an [`Environment`] containing convex optimization axioms and theorems.
645pub fn build_convex_optimization_env() -> Environment {
646    let mut env = Environment::new();
647    let axioms: &[(&str, Expr)] = &[
648        ("ConvexSet", convex_set_ty()),
649        ("ConvexFunction", convex_function_ty()),
650        ("KktConditions", kkt_conditions_ty()),
651        ("Lagrangian", lagrangian_ty()),
652        ("StrongDuality", strong_duality_ty()),
653        ("projection_theorem", projection_theorem_ty()),
654        ("supporting_hyperplane", supporting_hyperplane_ty()),
655        ("jensen_inequality", jensen_inequality_ty()),
656        ("slater_condition", slater_condition_ty()),
657        ("ConvexProgram", prop()),
658        ("DualProgram", prop()),
659        ("OptimalityGap", arrow(real_ty(), prop())),
660        ("FenchelConjugate", fenchel_conjugate_ty()),
661        (
662            "FenchelRockafellarDuality",
663            fenchel_rockafellar_duality_ty(),
664        ),
665        ("ConjugateSubgradient", conjugate_subgradient_ty()),
666        ("LagrangianDualFunction", lagrangian_dual_function_ty()),
667        ("LinearIndependenceCQ", licq_ty()),
668        ("MangasarianFromovitzCQ", mfcq_ty()),
669        ("ComplementarySlackness", complementary_slackness_ty()),
670        ("KktSufficiency", kkt_sufficiency_ty()),
671        ("BarrierFunction", barrier_function_ty()),
672        ("PathFollowingMethod", path_following_method_ty()),
673        ("PredictorCorrectorMethod", predictor_corrector_method_ty()),
674        ("CentralPathConvergence", central_path_convergence_ty()),
675        ("PositiveSemidefinite", positive_semidefinite_ty()),
676        ("SdpFeasibility", sdp_feasibility_ty()),
677        ("SdpDuality", sdp_duality_ty()),
678        ("SdpOptimality", sdp_optimality_ty()),
679        ("SecondOrderCone", second_order_cone_ty()),
680        ("SocpFeasibility", socp_feasibility_ty()),
681        ("Monomial", monomial_ty()),
682        ("Posynomial", posynomial_ty()),
683        ("GeometricProgramDuality", geometric_program_duality_ty()),
684        (
685            "SmoothGradientConvergence",
686            smooth_gradient_convergence_ty(),
687        ),
688        (
689            "StronglyConvexConvergence",
690            strongly_convex_convergence_ty(),
691        ),
692        ("ProximalOperator", proximal_operator_ty()),
693        ("IstaConvergence", ista_convergence_ty()),
694        ("FistaConvergence", fista_convergence_ty()),
695        ("ProximalGradientDescent", proximal_gradient_descent_ty()),
696        ("DouglasRachfordSplitting", douglas_rachford_splitting_ty()),
697        ("ChambollePockAlgorithm", chambolle_pock_ty()),
698        ("AugmentedLagrangian", augmented_lagrangian_ty()),
699        ("AdmmConvergence", admm_convergence_ty()),
700        ("SupportingHyperplaneCut", supporting_hyperplane_cut_ty()),
701        ("KelleyMethod", kelley_method_ty()),
702        ("BundleMethodConvergence", bundle_method_convergence_ty()),
703        (
704            "EllipsoidMethodComplexity",
705            ellipsoid_method_complexity_ty(),
706        ),
707        ("CenterOfGravityMethod", center_of_gravity_method_ty()),
708        ("SubgradientInequality", subgradient_inequality_ty()),
709        (
710            "SubgradientMethodConvergence",
711            subgradient_method_convergence_ty(),
712        ),
713        ("PolyakStepsize", polyak_stepsize_ty()),
714        ("SgdConvergence", sgd_convergence_ty()),
715        ("SvrgConvergence", svrg_convergence_ty()),
716        ("SarahConvergence", sarah_convergence_ty()),
717        ("SpiderConvergence", spider_convergence_ty()),
718        ("DcpAtomConvex", dcp_atom_convex_ty()),
719        ("DcpCompositionRule", dcp_composition_rule_ty()),
720        ("DcpVerification", dcp_verification_ty()),
721        ("SelfConcordantBarrier", self_concordant_barrier_ty()),
722        ("SelfConcordantComplexity", self_concordant_complexity_ty()),
723        ("LogarithmicBarrier", logarithmic_barrier_ty()),
724        ("NewtonDecrement", newton_decrement_ty()),
725        ("SdpSlaterCondition", sdp_slater_condition_ty()),
726        ("SdpComplementarity", sdp_complementarity_ty()),
727        ("SdpDualityGap", sdp_duality_gap_ty()),
728        ("LorentzCone", lorentz_cone_ty()),
729        ("SocpDuality", socp_duality_ty()),
730        ("RotatedLorentzCone", rotated_lorentz_cone_ty()),
731        ("AdmmLinearConvergence", admm_linear_convergence_ty()),
732        ("AdmmPrimalResidual", admm_primal_residual_ty()),
733        ("AdmmDualResidual", admm_dual_residual_ty()),
734        ("ProximalPointAlgorithm", proximal_point_algorithm_ty()),
735        ("ResolventOperator", resolvent_operator_ty()),
736        ("FirmlyNonexpansive", firmly_nonexpansive_ty()),
737        ("BregmanDivergence", bregman_divergence_ty()),
738        ("MirrorDescentConvergence", mirror_descent_convergence_ty()),
739        ("NegativeEntropyFunction", negative_entropy_function_ty()),
740        (
741            "ExponentialWeightsAlgorithm",
742            exponential_weights_algorithm_ty(),
743        ),
744        ("SagaConvergence", saga_convergence_ty()),
745        ("AdamConvergence", adam_convergence_ty()),
746        ("MomentumSgd", momentum_sgd_ty()),
747        ("MaximalMonotoneOperator", maximal_monotone_operator_ty()),
748        ("MonotoneInclusionProblem", monotone_inclusion_problem_ty()),
749        ("SplittingConvergence", splitting_convergence_ty()),
750        ("KantorovichProblem", kantorovich_problem_ty()),
751        ("KantorovichDuality", kantorovich_duality_ty()),
752        ("WassersteinDistance", wasserstein_distance_ty()),
753        ("SinkhornAlgorithm", sinkhorn_algorithm_ty()),
754        (
755            "RestrictedIsometryProperty",
756            restricted_isometry_property_ty(),
757        ),
758        ("BasisPursuitRecovery", basis_pursuit_recovery_ty()),
759        ("LassoSparsity", lasso_sparsity_ty()),
760        ("NuclearNorm", nuclear_norm_ty()),
761        ("MatrixCompletionTheorem", matrix_completion_theorem_ty()),
762        ("RobustPca", robust_pca_ty()),
763        ("ChanceConstraint", chance_constraint_ty()),
764        (
765            "DistributionallyRobustObjective",
766            distributionally_robust_objective_ty(),
767        ),
768        ("WassersteinAmbiguitySet", wasserstein_ambiguity_set_ty()),
769        ("CvarConstraint", cvar_constraint_ty()),
770        ("OnlineConvexOptimization", online_convex_optimization_ty()),
771        ("FtrlRegretBound", ftrl_regret_bound_ty()),
772        ("AdaptiveRegretBound", adaptive_regret_bound_ty()),
773        (
774            "OnlineGradientDescentRegret",
775            online_gradient_descent_regret_ty(),
776        ),
777    ];
778    for (name, ty) in axioms {
779        env.add(Declaration::Axiom {
780            name: Name::str(*name),
781            univ_params: vec![],
782            ty: ty.clone(),
783        })
784        .ok();
785    }
786    env
787}
788/// Trait for convex functions over ℝ^n.
789pub trait ConvexFunction {
790    /// Evaluate f(x).
791    fn eval(&self, x: &[f64]) -> f64;
792    /// Compute the gradient ∇f(x).
793    fn gradient(&self, x: &[f64]) -> Vec<f64>;
794    /// Return `true` if f is strongly convex.
795    fn is_strongly_convex(&self) -> bool;
796}
797/// Trait for functions with a computable proximal operator.
798pub trait ProxableFunction: ConvexFunction {
799    /// prox_{t·self}(v) = argmin_x { self(x) + 1/(2t) ‖x-v‖² }.
800    fn prox(&self, v: &[f64], t: f64) -> Vec<f64>;
801}
802#[cfg(test)]
803mod tests {
804    use super::*;
805    #[test]
806    fn test_quadratic_eval_origin() {
807        let q = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
808        let f = QuadraticFunction::new(q, vec![0.0, 0.0], 0.0);
809        assert!((f.eval(&[0.0, 0.0])).abs() < 1e-12);
810    }
811    #[test]
812    fn test_quadratic_eval_nonzero() {
813        let q = vec![vec![2.0]];
814        let f = QuadraticFunction::new(q, vec![0.0], 0.0);
815        assert!((f.eval(&[2.0]) - 4.0).abs() < 1e-9);
816    }
817    #[test]
818    fn test_quadratic_gradient() {
819        let q = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
820        let f = QuadraticFunction::new(q, vec![0.0, 0.0], 0.0);
821        let grad = f.gradient(&[3.0, -1.0]);
822        assert!((grad[0] - 3.0).abs() < 1e-9);
823        assert!((grad[1] + 1.0).abs() < 1e-9);
824    }
825    #[test]
826    fn test_strongly_convex() {
827        let q = vec![vec![2.0, 0.0], vec![0.0, 3.0]];
828        let f = QuadraticFunction::new(q, vec![0.0, 0.0], 0.0);
829        assert!(f.is_strongly_convex());
830    }
831    #[test]
832    fn test_gradient_descent_minimizes_quadratic() {
833        let q = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
834        let f = QuadraticFunction::new(q, vec![0.0, 0.0], 0.0);
835        let gd = GradientDescent::new(0.1, 500, 1e-6);
836        let (x, fval, _iters) = gd.minimize(&f, &[5.0, -3.0]);
837        assert!(fval < 1e-6, "fval={fval}");
838        assert!(x[0].abs() < 1e-3);
839        assert!(x[1].abs() < 1e-3);
840    }
841    #[test]
842    fn test_projected_gradient_box_constraint() {
843        let q = vec![vec![1.0]];
844        let f = QuadraticFunction::new(q, vec![0.0], 0.0);
845        let pg = ProjectedGradient::new(0.1, 300, 1e-6, vec![1.0], vec![5.0]);
846        let (x, fval) = pg.minimize(&f, &[4.0]);
847        assert!((x[0] - 1.0).abs() < 1e-3, "x={}", x[0]);
848        assert!((fval - 0.5).abs() < 1e-3, "fval={fval}");
849    }
850    #[test]
851    fn test_admm_solve_lasso_stub() {
852        let a = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
853        let b = vec![1.0, 2.0];
854        let admm = ADMM::new(1.0);
855        let x = admm.solve_lasso(&a, &b, 0.1);
856        assert_eq!(x.len(), 2);
857        assert_eq!(x, vec![0.0, 0.0]);
858    }
859    #[test]
860    fn test_build_convex_optimization_env() {
861        let env = build_convex_optimization_env();
862        assert!(env.get(&Name::str("ConvexSet")).is_some());
863        assert!(env.get(&Name::str("ConvexFunction")).is_some());
864        assert!(env.get(&Name::str("KktConditions")).is_some());
865        assert!(env.get(&Name::str("projection_theorem")).is_some());
866        assert!(env.get(&Name::str("jensen_inequality")).is_some());
867        assert!(env.get(&Name::str("FenchelConjugate")).is_some());
868        assert!(env.get(&Name::str("FenchelRockafellarDuality")).is_some());
869        assert!(env.get(&Name::str("PositiveSemidefinite")).is_some());
870        assert!(env.get(&Name::str("SdpDuality")).is_some());
871        assert!(env.get(&Name::str("FistaConvergence")).is_some());
872        assert!(env.get(&Name::str("ProximalOperator")).is_some());
873        assert!(env.get(&Name::str("DouglasRachfordSplitting")).is_some());
874        assert!(env.get(&Name::str("ChambollePockAlgorithm")).is_some());
875        assert!(env.get(&Name::str("EllipsoidMethodComplexity")).is_some());
876        assert!(env.get(&Name::str("SvrgConvergence")).is_some());
877        assert!(env.get(&Name::str("SpiderConvergence")).is_some());
878        assert!(env.get(&Name::str("DcpVerification")).is_some());
879    }
880    #[test]
881    fn test_l1_norm_prox_soft_threshold() {
882        let g = L1NormFunction::new(1.0);
883        let result = g.prox(&[3.0, -0.5], 1.0);
884        assert!((result[0] - 2.0).abs() < 1e-12, "result[0]={}", result[0]);
885        assert!(result[1].abs() < 1e-12, "result[1]={}", result[1]);
886    }
887    #[test]
888    fn test_fista_minimizes_smooth_quadratic() {
889        let smooth = QuadraticFunction::new(vec![vec![1.0]], vec![0.0], 0.0);
890        let reg = L1NormFunction::new(0.0);
891        let solver = FISTASolver::new(1.0, 200, 1e-6);
892        let (x, _iters) = solver.minimize(&smooth, &reg, &[5.0]);
893        assert!(x[0].abs() < 1e-3, "x[0]={}", x[0]);
894    }
895    #[test]
896    fn test_sdp_relaxation_psd_check() {
897        let id = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
898        assert!(SDPRelaxation::is_psd(&id));
899        let neg = vec![vec![-1.0, 0.0], vec![0.0, 1.0]];
900        assert!(!SDPRelaxation::is_psd(&neg));
901    }
902    #[test]
903    fn test_sdp_relaxation_solve_returns_bound() {
904        let q = vec![vec![2.0, 0.0], vec![0.0, 2.0]];
905        let c = vec![0.0, 0.0];
906        let a = vec![vec![1.0, 0.0]];
907        let b = vec![1.0];
908        let sdp = SDPRelaxation::new(q, c, a, b);
909        let bound = sdp.solve();
910        assert!((bound - 0.0).abs() < 1e-12);
911    }
912    #[test]
913    fn test_geometric_program_log_sum_exp() {
914        let monomials = vec![(0.0_f64, vec![1.0_f64])];
915        let lse = GeometricProgramSolver::log_sum_exp_posynomial(&monomials, &[1.0]);
916        assert!((lse - 1.0).abs() < 1e-9, "lse={lse}");
917    }
918    #[test]
919    fn test_cutting_plane_minimizes_quadratic() {
920        let f = QuadraticFunction::new(vec![vec![2.0]], vec![0.0], 0.0);
921        let solver = CuttingPlaneSolver::new(100, 1e-4, 2.0);
922        let (x, fval, _iters) = solver.minimize(&f, &[3.0]);
923        assert!(fval < 1.0, "fval={fval}");
924        let _ = x;
925    }
926    #[test]
927    fn test_bundle_method_minimizes_quadratic() {
928        let f = QuadraticFunction::new(vec![vec![2.0]], vec![0.0], 0.0);
929        let solver = BundleMethodSolver::new(1.0, 0.5, 20, 200, 1e-5);
930        let (x, fval, _iters) = solver.minimize(&f, &[4.0]);
931        assert!(fval < 1.0, "fval={fval}");
932        let _ = x;
933    }
934    #[test]
935    fn test_new_axioms_in_env() {
936        let env = build_convex_optimization_env();
937        assert!(env.get(&Name::str("SelfConcordantBarrier")).is_some());
938        assert!(env.get(&Name::str("SelfConcordantComplexity")).is_some());
939        assert!(env.get(&Name::str("LogarithmicBarrier")).is_some());
940        assert!(env.get(&Name::str("NewtonDecrement")).is_some());
941        assert!(env.get(&Name::str("SdpSlaterCondition")).is_some());
942        assert!(env.get(&Name::str("SdpComplementarity")).is_some());
943        assert!(env.get(&Name::str("SdpDualityGap")).is_some());
944        assert!(env.get(&Name::str("LorentzCone")).is_some());
945        assert!(env.get(&Name::str("SocpDuality")).is_some());
946        assert!(env.get(&Name::str("RotatedLorentzCone")).is_some());
947        assert!(env.get(&Name::str("AdmmLinearConvergence")).is_some());
948        assert!(env.get(&Name::str("AdmmPrimalResidual")).is_some());
949        assert!(env.get(&Name::str("AdmmDualResidual")).is_some());
950        assert!(env.get(&Name::str("ProximalPointAlgorithm")).is_some());
951        assert!(env.get(&Name::str("ResolventOperator")).is_some());
952        assert!(env.get(&Name::str("FirmlyNonexpansive")).is_some());
953        assert!(env.get(&Name::str("BregmanDivergence")).is_some());
954        assert!(env.get(&Name::str("MirrorDescentConvergence")).is_some());
955        assert!(env.get(&Name::str("NegativeEntropyFunction")).is_some());
956        assert!(env.get(&Name::str("ExponentialWeightsAlgorithm")).is_some());
957        assert!(env.get(&Name::str("SagaConvergence")).is_some());
958        assert!(env.get(&Name::str("AdamConvergence")).is_some());
959        assert!(env.get(&Name::str("MomentumSgd")).is_some());
960        assert!(env.get(&Name::str("MaximalMonotoneOperator")).is_some());
961        assert!(env.get(&Name::str("MonotoneInclusionProblem")).is_some());
962        assert!(env.get(&Name::str("SplittingConvergence")).is_some());
963        assert!(env.get(&Name::str("KantorovichProblem")).is_some());
964        assert!(env.get(&Name::str("KantorovichDuality")).is_some());
965        assert!(env.get(&Name::str("WassersteinDistance")).is_some());
966        assert!(env.get(&Name::str("SinkhornAlgorithm")).is_some());
967        assert!(env.get(&Name::str("RestrictedIsometryProperty")).is_some());
968        assert!(env.get(&Name::str("BasisPursuitRecovery")).is_some());
969        assert!(env.get(&Name::str("LassoSparsity")).is_some());
970        assert!(env.get(&Name::str("NuclearNorm")).is_some());
971        assert!(env.get(&Name::str("MatrixCompletionTheorem")).is_some());
972        assert!(env.get(&Name::str("RobustPca")).is_some());
973        assert!(env.get(&Name::str("ChanceConstraint")).is_some());
974        assert!(env
975            .get(&Name::str("DistributionallyRobustObjective"))
976            .is_some());
977        assert!(env.get(&Name::str("WassersteinAmbiguitySet")).is_some());
978        assert!(env.get(&Name::str("CvarConstraint")).is_some());
979        assert!(env.get(&Name::str("OnlineConvexOptimization")).is_some());
980        assert!(env.get(&Name::str("FtrlRegretBound")).is_some());
981        assert!(env.get(&Name::str("AdaptiveRegretBound")).is_some());
982        assert!(env.get(&Name::str("OnlineGradientDescentRegret")).is_some());
983    }
984    #[test]
985    fn test_mirror_descent_project_simplex() {
986        let v = vec![0.5, 0.5];
987        let p = MirrorDescentSolver::project_simplex(&v);
988        assert!((p.iter().sum::<f64>() - 1.0).abs() < 1e-9);
989        assert!(p.iter().all(|&x| x >= 0.0));
990    }
991    #[test]
992    fn test_mirror_descent_simplex_sum_to_one() {
993        let v = vec![3.0, -1.0, 2.0];
994        let p = MirrorDescentSolver::project_simplex(&v);
995        assert!((p.iter().sum::<f64>() - 1.0).abs() < 1e-9);
996        assert!(p.iter().all(|&x| x >= 0.0));
997    }
998    #[test]
999    fn test_mirror_descent_bregman_kl_zero() {
1000        let x = vec![0.25, 0.25, 0.5];
1001        let kl = MirrorDescentSolver::bregman_kl(&x, &x);
1002        assert!(kl.abs() < 1e-10, "kl={kl}");
1003    }
1004    #[test]
1005    fn test_mirror_descent_minimizes_quadratic() {
1006        let f = QuadraticFunction::new(vec![vec![1.0]], vec![0.0], 0.0);
1007        let solver = MirrorDescentSolver::new(0.05, 500, 1e-6, false);
1008        let (x, fval, _iters) = solver.minimize(&f, &[3.0]);
1009        assert!(fval < 0.1, "fval={fval}");
1010        let _ = x;
1011    }
1012    #[test]
1013    fn test_proximal_gradient_ista_minimizes() {
1014        let smooth = QuadraticFunction::new(vec![vec![2.0]], vec![0.0], 0.0);
1015        let reg = L1NormFunction::new(0.0);
1016        let solver = ProximalGradientSolver::new(2.0, 300, 1e-7, false);
1017        let (x, iters) = solver.minimize(&smooth, &reg, &[5.0]);
1018        assert!(x[0].abs() < 0.01, "x[0]={}", x[0]);
1019        let _ = iters;
1020    }
1021    #[test]
1022    fn test_proximal_gradient_fista_accelerated() {
1023        let smooth = QuadraticFunction::new(vec![vec![2.0]], vec![0.0], 0.0);
1024        let reg = L1NormFunction::new(0.0);
1025        let solver_fista = ProximalGradientSolver::new(2.0, 200, 1e-7, true);
1026        let solver_ista = ProximalGradientSolver::new(2.0, 200, 1e-7, false);
1027        let (x_fista, iters_fista) = solver_fista.minimize(&smooth, &reg, &[5.0]);
1028        let (x_ista, iters_ista) = solver_ista.minimize(&smooth, &reg, &[5.0]);
1029        assert!(
1030            iters_fista <= iters_ista + 10,
1031            "fista={iters_fista}, ista={iters_ista}"
1032        );
1033        assert!(x_fista[0].abs() < 0.01, "x_fista={}", x_fista[0]);
1034        let _ = x_ista;
1035    }
1036    #[test]
1037    fn test_proximal_gradient_estimate_lipschitz() {
1038        let f = QuadraticFunction::new(vec![vec![2.0]], vec![0.0], 0.0);
1039        let l_est = ProximalGradientSolver::estimate_lipschitz(&f, &[1.0], 1);
1040        assert!(l_est > 0.5, "L_est={l_est}");
1041    }
1042    #[test]
1043    fn test_sinkhorn_uniform_transport() {
1044        let mu = vec![0.5, 0.5];
1045        let nu = vec![0.5, 0.5];
1046        let cost = vec![vec![0.0, 1.0], vec![1.0, 0.0]];
1047        let solver = SinkhornSolver::new(0.1, 200, 1e-8);
1048        let (gamma, w) = solver.solve(&mu, &nu, &cost);
1049        let total: f64 = gamma.iter().flat_map(|r| r.iter()).sum();
1050        assert!((total - 1.0).abs() < 1e-4, "total={total}");
1051        assert!(w >= 0.0, "w={w}");
1052    }
1053    #[test]
1054    fn test_sinkhorn_same_distribution() {
1055        let mu = vec![0.5, 0.5];
1056        let nu = vec![0.5, 0.5];
1057        let cost = vec![vec![0.0, 1.0], vec![1.0, 0.0]];
1058        let solver = SinkhornSolver::new(0.01, 500, 1e-10);
1059        let (_gamma, w) = solver.solve(&mu, &nu, &cost);
1060        assert!(w < 0.6, "w={w}");
1061    }
1062    #[test]
1063    fn test_sinkhorn_wasserstein2_1d_zero() {
1064        let pts = vec![0.0, 1.0];
1065        let wts = vec![0.5, 0.5];
1066        let w2 = SinkhornSolver::wasserstein2_1d(&pts, &wts, &pts, &wts);
1067        assert!(w2 < 0.2, "w2={w2}");
1068    }
1069    #[test]
1070    fn test_rip_identity_satisfies_rip() {
1071        let id = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
1072        let verifier = RipVerifier::new(1, 10);
1073        let (dl, du) = verifier.estimate_rip_constant(&id);
1074        assert!(du < 0.01, "delta_upper={du}");
1075        let _ = dl;
1076    }
1077    #[test]
1078    fn test_rip_soft_threshold() {
1079        let x = vec![3.0, -0.5, 0.2];
1080        let result = RipVerifier::soft_threshold(&x, 1.0);
1081        assert!((result[0] - 2.0).abs() < 1e-12);
1082        assert!(result[1].abs() < 1e-12);
1083        assert!(result[2].abs() < 1e-12);
1084    }
1085    #[test]
1086    fn test_rip_satisfies_rip_check() {
1087        let id = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
1088        let verifier = RipVerifier::new(1, 5);
1089        assert!(verifier.satisfies_rip(&id, 0.5));
1090    }
1091    #[test]
1092    fn test_online_learner_initial_decision() {
1093        let learner = OnlineLearner::new(0.1, 3);
1094        let x = learner.current_decision();
1095        assert_eq!(x.len(), 3);
1096        assert!(x.iter().all(|&xi| xi.abs() < 1e-12));
1097    }
1098    #[test]
1099    fn test_online_learner_update_accumulates() {
1100        let mut learner = OnlineLearner::new(0.1, 2);
1101        learner.update(&[1.0, 0.0]);
1102        let x = learner.current_decision();
1103        assert!((x[0] + 0.1).abs() < 1e-9, "x[0]={}", x[0]);
1104        assert!(x[1].abs() < 1e-9, "x[1]={}", x[1]);
1105    }
1106    #[test]
1107    fn test_online_learner_regret_bound_positive() {
1108        let mut learner = OnlineLearner::new(0.01, 2);
1109        for _ in 0..10 {
1110            learner.update(&[0.5, -0.5]);
1111        }
1112        let bound = learner.regret_bound(1.0, 1.0);
1113        assert!(bound >= 0.0, "bound={bound}");
1114    }
1115    #[test]
1116    fn test_online_learner_reset() {
1117        let mut learner = OnlineLearner::new(0.1, 2);
1118        learner.update(&[1.0, 2.0]);
1119        learner.reset();
1120        assert_eq!(learner.round, 0);
1121        let x = learner.current_decision();
1122        assert!(x.iter().all(|&xi| xi.abs() < 1e-12));
1123    }
1124}
oxilean_std/convex_optimization/functions.rs

oxilean_std/convex_optimization/
functions.rs
