LeanPool.Duality.FarkasSpecial

def «term__∞» : Lean.ParserDescr

F∞ is sugar for Extend F, the type of values in F ∪ {⊥, ⊤}.

Equations

• One or more equations did not get rendered due to their size.

def unexpandExtend : Lean.PrettyPrinter.Unexpander

Pretty-print Extend F back as F∞.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev NNeg (F : Type u_1) [Zero F] [LE F] : Type u_1

NNeg F is the subtype of nonnegative elements of F.

Equations

• F≥0 = { a : F // 0 ≤ a }

def «term__≥0» : Lean.ParserDescr

F≥0 is sugar for NNeg F, the subtype of nonnegative elements of F.

Equations

• One or more equations did not get rendered due to their size.

def unexpandNNeg : Lean.PrettyPrinter.Unexpander

Pretty-print NNeg F back as F≥0.

Equations

• One or more equations did not get rendered due to their size.

def EF.smulNN {F : Type u_1} [Field F] [LinearOrder F] (c : F≥0) : F∞ → F∞

Scalar action of a nonnegative scalar on F∞: c • ⊥ = ⊥, c • ⊤ = ⊤ when c > 0 (and c • ⊤ = 0 when c = 0), and c • (f : F) = c * f on finite values.

Equations

• EF.smulNN c none = ⊥
• EF.smulNN c (some none) = if c = 0 then 0 else ⊤
• EF.smulNN c (some (some f)) = ↑(↑c * f)

@[implicit_reducible]

instance instSMulZeroClassNNegExtend {F : Type u_1} [Field F] [LinearOrder F] : SMulZeroClass F≥0 F∞

Equations

• instSMulZeroClassNNegExtend = { smul := EF.smulNN, smul_zero := ⋯ }

theorem EF.pos_smul_top {F : Type u_1} [Field F] [LinearOrder F] {c : F≥0} (hc : 0 < c) : c • ⊤ = ⊤

theorem EF.smul_top_neq_bot {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (c : F≥0) : c • ⊤ ≠ ⊥

theorem EF.smul_coe_neq_bot {F : Type u_1} [Field F] [LinearOrder F] (c : F≥0) (f : F) : c • ↑f ≠ ⊥

theorem EF.smul_bot {F : Type u_1} [Field F] [LinearOrder F] (c : F≥0) : c • ⊥ = ⊥

theorem EF.smul_nonbot_neq_bot {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (c : F≥0) {r : F∞} (hr : r ≠ ⊥) : c • r ≠ ⊥

theorem EF.zero_smul_nonbot {F : Type u_1} [Field F] [LinearOrder F] {r : F∞} (hr : r ≠ ⊥) : 0 • r = 0

theorem EF.zero_smul_coe {F : Type u_1} [Field F] [LinearOrder F] (f : F) : 0 • ↑f = 0

def EF.AddHom {F : Type u_1} [Field F] : F →+ F∞

The canonical inclusion F → F∞ packaged as an additive homomorphism.

Equations

• EF.AddHom = { toFun := toE, map_zero' := ⋯, map_add' := ⋯ }

theorem Finset.sum_toE {F : Type u_1} [Field F] {ι : Type u_2} (s : Finset ι) (f : ι → F) : ↑(s.sum f) = ∑ i ∈ s, ↑(f i)

theorem Multiset.sum_eq_EF_bot_iff {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (s : Multiset F∞) : s.sum = ⊥ ↔ ⊥ ∈ s

theorem Multiset.sum_eq_EF_top {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {s : Multiset F∞} (htop : ⊤ ∈ s) (hbot : ⊥ ∉ s) : s.sum = ⊤

def dotWeig {I : Type u_2} [Fintype I] {α : Type u_4} {γ : Type u_5} [AddCommMonoid α] [SMul γ α] (v : I → α) (w : I → γ) : α

dotWeig v w is the sum of the element-wise products w i • v i akin the dot product but heterogeneous (mnemonic: "vector times weights"). Note that the order of arguments (also with the infix notation) is opposite than in the SMul it builds upon.

Equations

• v ᵥ⬝ w = ∑ i : I, w i • v i

def «term_ᵥ⬝_» : Lean.TrailingParserDescr

dotWeig v w is the sum of the element-wise products w i • v i akin the dot product but heterogeneous (mnemonic: "vector times weights"). Note that the order of arguments (also with the infix notation) is opposite than in the SMul it builds upon.

Equations

• «term_ᵥ⬝_» = Lean.ParserDescr.trailingNode `«term_ᵥ⬝_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᵥ⬝ ") (Lean.ParserDescr.cat `term 73))

def Matrix.mulWeig {I : Type u_2} {J : Type u_3} [Fintype J] {α : Type u_4} {γ : Type u_5} [AddCommMonoid α] [SMul γ α] (M : Matrix I J α) (w : J → γ) (i : I) : α

Matrix.mulWeig M w is the heterogeneous analogue of the matrix-vector product Matrix.mulVec M w (mnemonic: "matrix times weights"). Note that the order of arguments (also with the infix notation) is opposite than in the SMul it builds upon.

Equations

• (M ₘ* w) i = M i ᵥ⬝ w

def «term_ₘ*_» : Lean.TrailingParserDescr

Matrix.mulWeig M w is the heterogeneous analogue of the matrix-vector product Matrix.mulVec M w (mnemonic: "matrix times weights"). Note that the order of arguments (also with the infix notation) is opposite than in the SMul it builds upon.

Equations

• «term_ₘ*_» = Lean.ParserDescr.trailingNode `«term_ₘ*_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ₘ* ") (Lean.ParserDescr.cat `term 73))

theorem no_bot_dotWeig_zero {F : Type u_1} [Field F] [LinearOrder F] {I : Type u_2} [Fintype I] {v : I → F∞} (hv : ∀ (i : I), v i ≠ ⊥) : v ᵥ⬝ 0 = 0

theorem has_bot_dotWeig_nneg {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} [Fintype I] {v : I → F∞} {i : I} (hvi : v i = ⊥) (w : I → F≥0) : v ᵥ⬝ w = ⊥

theorem no_bot_dotWeig_nneg {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} [Fintype I] {v : I → F∞} (hv : ∀ (i : I), v i ≠ ⊥) (w : I → F≥0) : v ᵥ⬝ w ≠ ⊥

theorem no_bot_has_top_dotWeig_pos {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} [Fintype I] {v : I → F∞} (hv : ∀ (a : I), v a ≠ ⊥) {i : I} (hvi : v i = ⊤) (w : I → F≥0) (hwi : 0 < w i) : v ᵥ⬝ w = ⊤

theorem no_bot_has_top_dotWeig_le {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} [Fintype I] {v : I → F∞} (hv : ∀ (a : I), v a ≠ ⊥) {i : I} (hvi : v i = ⊤) (w : I → F≥0) {f : F} (hq : v ᵥ⬝ w ≤ ↑f) : w i ≤ 0

theorem no_bot_has_top_dotWeig_nneg_le {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} [Fintype I] {v : I → F∞} (hv : ∀ (a : I), v a ≠ ⊥) {i : I} (hvi : v i = ⊤) (w : I → F≥0) {f : F} (hq : v ᵥ⬝ w ≤ ↑f) : w i = 0

theorem dotWeig_zero_le_zero {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} [Fintype I] (v : I → F∞) : v ᵥ⬝ 0 ≤ 0

theorem Matrix.mulWeig_zero_le_zero {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} {J : Type u_3} [Fintype J] (M : Matrix I J F∞) : M ₘ* 0 ≤ 0

The proof of extendedFarkas below is split across several private helpers so that no single proof body exceeds the LeanPool 200-line cap, and so the elaborator does not run out of heartbeats.

theorem extendedFarkas {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] (A : Matrix I J F∞) (b : I → F∞) (hAi : ¬∃ (i : I), (∃ (j : J), A i j = ⊥) ∧ ∃ (j : J), A i j = ⊤) (hAj : ¬∃ (j : J), (∃ (i : I), A i j = ⊥) ∧ ∃ (i : I), A i j = ⊤) (hAb : ¬∃ (i : I), (∃ (j : J), A i j = ⊤) ∧ b i = ⊤) (hbA : ¬∃ (i : I), (∃ (j : J), A i j = ⊥) ∧ b i = ⊥) : (∃ (x : J → F≥0), A ₘ* x ≤ b) ≠ ∃ (y : I → F≥0), -A.transpose ₘ* y ≤ 0 ∧ b ᵥ⬝ y < 0

Just like inequalityFarkas_neg but for A and b over F∞.