Linear programming according to Antoine Chambert-Loir's book — affine version #10159
Conversation
| /-- Linear map -/ | ||
| linmap : M →ᵃ[R] N | ||
| /-- Right-hand side -/ | ||
| upper : N |
There was a problem hiding this comment.
There's no need for upper here, the point of the affine refactor is that it becomes part of linmap.
There was a problem hiding this comment.
When I refactored it to not use upper, it ended up looking very strange:
/-- Typically `M` is `ℝ^m` and `N` is `ℝ^n` -/
structure LinearProgram (R V M N : Type*) [OrderedRing R]
[AddCommGroup V] [Module R V] [AddTorsor V M]
[AddCommGroup N] [Module R N]
where
/-- Affine map -/
themap : M →ᵃ[R] N
/-- Objective function -/
objective : M →ᵃ[R] R
/-- Cone defines nonnegative elements -/
cone : PointedCone R N
variable {R V W M N : Type*} [OrderedRing R]
[AddCommGroup V] [Module R V] [AddTorsor V M]
[AddCommGroup N] [Module R N]
/-- `LP.primal = { x : M | LP.themap x ≤ LP.upper }` -/
def LinearProgram.primal (LP : LinearProgram R V M N) :=
{ x : M | -LP.themap x ∈ LP.cone }
/-- `LP.dual = { g : N →ᵃ[R] R | LP.objective = g ∘ LP.themap ∧ ∀ a, ∀ b, a ≤ b → g a ≤ g b }` -/
def LinearProgram.dual (LP : LinearProgram R V M N) :=
{ g : N →ᵃ[R] R | LP.objective = g ∘ LP.themap ∧
∀ a : N, ∀ b : N, (b -ᵥ a) ∈ LP.cone → g a ≤ g b }
-- From here on, we will need more assumptions than currently written
theorem LinearProgram.weakDuality (LP : LinearProgram R V M N)
{c : M} (hc : c ∈ LP.primal) {d : N →ᵃ[R] R} (hd : d ∈ LP.dual) :
LP.objective c ≤ d 0 := by
simp_all [LinearProgram.primal, LinearProgram.dual]
Since we are maximizing in the primal, the feasibility condition ends up being { x : M | -LP.themap x ∈ LP.cone }, which is ugly af.
There was a problem hiding this comment.
If you really want me to do it, I can flip the sign and proceed with this setting, but I am not happy about it, since we seemed to finally reached the consensus that Antoine Chambert-Loir's definition is the one we want to have in Mathlib.
| /-- Typically `M` is `ℝ^m` and `N` is `ℝ^n` -/ | ||
| structure LinearProgram (R V W M N : Type*) [OrderedRing R] | ||
| [AddCommGroup V] [Module R V] [AddTorsor V M] | ||
| [AddCommGroup W] [Module R W] [AddTorsor W N] | ||
| where |
There was a problem hiding this comment.
My original suggestion was only that M should be affine, not N. I don't really understand what N is (you didn't write any documentation!), but M is natural space in which the problem is set up, which may as well be affine
There was a problem hiding this comment.
I am familiar with finite-dimensional setting. In finite-dimensional setting, where LP is typically represented by a matrix, my M represents variables and my N represents conditions.
There was a problem hiding this comment.
For me personally, modelling LP in my head is easier in terms of "searching for a vector" than "searching for a point". I understand that "searching for a point" has certain appeal and I am therefore willing to rephrase the definitions to the affine setting; however, if M should be be affine, I will make N affine as well, so that the dual of LP is still kinda LP.
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)