linear programming

Stream: maths

[Arthur Paulino]

Do we have formalized content on linear programming? I'm searching through mathlib docs but I can't find it

[Martin Dvořák]

No.

[Yaël Dillies]

analysis.convex. contains all the convexity stuff, but there isn't much more than that, no.

[Apurva Nakade]

Hello, is there anyone working on linear programming? My summer break has just started and I'm looking for a short project to do. I'm thinking of adding 1) hyperplane separation, 2) Farkas' lemma, 3) Weak duality, 4) Strong duality (both dualities only for linear programs only).

[Yaël Dillies]

Isn't hyperplane separation docs#geometric_hahn_banach_closed_compact?

[Yaël Dillies]

I also have Stone's separation in #14677, but that's probably not what you want.

[Apurva Nakade]

Yaël Dillies said:

Isn't hyperplane separation docs#geometric_hahn_banach_closed_compact?

Yes, thanks! :)

[Alexander Bentkamp]

@Apurva Nakade I have some old code here formalizing the duality theorem for cone programs (https://github.com/abentkamp/duality, see cone_duality in src/cone_program.lean). Maybe you are better off starting from scratch though because the code is very old and goes beyond linear programming.

[Apurva Nakade]

Thank you, this is very helpful! It helps me see that conic programming is the easiest to code. I suspect that most of the auxiliary files you have are already in mathlib. I'll try to see adapt cone_program.lean to the current mathlib.