LeanPool.Duality.FarkasBartl #
theorem
industepFarkasBartl
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{m : ℕ}
[DivisionRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[AddCommGroup V]
[LinearOrder V]
[IsOrderedAddMonoid V]
[Module R V]
[PosSMulMono R V]
[AddCommGroup W]
[Module R W]
(ih :
∀ (A₀ : W →ₗ[R] Fin m → R) (b₀ : W →ₗ[R] V),
(∀ (y₀ : W), 0 ≤ A₀ y₀ → 0 ≤ b₀ y₀) →
∃ (x₀ : Fin m → V), 0 ≤ x₀ ∧ ∀ (w₀ : W), ∑ i₀ : Fin m, A₀ w₀ i₀ • x₀ i₀ = b₀ w₀)
{A : W →ₗ[R] Fin m.succ → R}
{b : W →ₗ[R] V}
(hAb : ∀ (y : W), 0 ≤ A y → 0 ≤ b y)
:
theorem
finFarkasBartl
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{n : ℕ}
[DivisionRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[AddCommGroup V]
[LinearOrder V]
[IsOrderedAddMonoid V]
[Module R V]
[PosSMulMono R V]
[AddCommGroup W]
[Module R W]
(A : W →ₗ[R] Fin n → R)
(b : W →ₗ[R] V)
:
theorem
fintypeFarkasBartl
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{J : Type u_4}
[Fintype J]
[DivisionRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[AddCommGroup V]
[LinearOrder V]
[IsOrderedAddMonoid V]
[Module R V]
[PosSMulMono R V]
[AddCommGroup W]
[Module R W]
(A : W →ₗ[R] J → R)
(b : W →ₗ[R] V)
:
theorem
almostFarkasBartl
{R : Type u_1}
{W : Type u_3}
{J : Type u_4}
[Fintype J]
[DivisionRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[AddCommGroup W]
[Module R W]
(A : W →ₗ[R] J → R)
(b : W →ₗ[R] R)
:
theorem
coordinateFarkasBartl
{R : Type u_1}
{I : Type u_4}
{J : Type u_5}
[Fintype J]
[DivisionRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
(A : (I → R) →ₗ[R] J → R)
(b : (I → R) →ₗ[R] R)
: