Linear programming according to Antoine Chambert-Loir's book #10026
Conversation
madvorak
changed the title
|
|
||
| /-- Typically `M` is `ℝ^m` and `N` is `ℝ^n` -/ | ||
| structure LinearProgram (R : Type*) (M : Type*) (N : Type*) | ||
| [OrderedSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] where |
There was a problem hiding this comment.
I think it probably makes sense to generalize M to an affine space, though I guess you'd be trading no negation for no origin, as we don't have a typeclass that means neither...
There was a problem hiding this comment.
Is there any literature for the theory of linear programming over affine spaces?
There was a problem hiding this comment.
In my experience it's uncommon to require that the objective be zero at the origin; especially since often when a function is described as "linear" it really means "affine"
There was a problem hiding this comment.
Aren't we talking about two different things at the same time?
The first thing, which is a pretty small change, is to allow affine functions in addition to linear functions in the objective.
The second thing, which is quite nontrivial, is to deny that the space of solutions contains some zero solution (which may be infeasible), even if the objective value for zero solution is not required to be zero.
There was a problem hiding this comment.
Sketch what it could look like with affine stuff:
#10159
|
If this PR is not ready for review can you label it WIP please? Thanks! |
riccardobrasca
added
the
awaiting-author
Instead of RFC, or in addition to RFC? |
In addition. We are thinking about a different way of managing PRs and we would like to use more ofter "WIP" (I think you have a couple of other PRs in the same state). Thanks! |
OK, I will label all four LP PRs with WIP in addition to RFC. |
madvorak
added
WIP
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.237386.20Linear.20Programming
Four PRs incompatible with each other:
#7386 (list of constraints)
#9693 (matrix form)
#10026 (Antoine Chambert-Loir's def; semirings, linear)
#10159 (Antoine Chambert-Loir's def; rings, affine)