More WIP

GuiBrandt · Sep 25, 2024 · 43f5520 · 43f5520
1 parent 90194f9
commit 43f5520
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 12 deletions.
diff --git a/PolyhedralCombinatorics/Projection/Computable.lean b/PolyhedralCombinatorics/Projection/Computable.lean
@@ -28,9 +28,21 @@ def projectionMatrix (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) :=
       | .inr (s, t) => Pi.single ↑s (S.mat t ⬝ᵥ c) - Pi.single ↑t (S.mat s ⬝ᵥ c)
   U
 
-abbrev transform (S : LinearSystem 𝔽 n) {r : ℕ} (T : Matrix (Fin r) (Fin S.m) 𝔽)
+def transform (S : LinearSystem 𝔽 n) {r : ℕ} (T : Matrix (Fin r) (Fin S.m) 𝔽)
   : LinearSystem 𝔽 n := of (T * S.mat) (T *ᵥ S.vec)
 
+@[simp]
+theorem transform_m (S : LinearSystem 𝔽 n) {r} (T : Matrix (Fin r) (Fin S.m) 𝔽)
+  : (S.transform T).m = r := rfl
+
+@[simp]
+theorem transform_mat (S : LinearSystem 𝔽 n) {r} (T : Matrix (Fin r) (Fin S.m) 𝔽)
+  : (S.transform T).mat = T * S.mat := rfl
+
+@[simp]
+theorem transform_vec (S : LinearSystem 𝔽 n) {r} (T : Matrix (Fin r) (Fin S.m) 𝔽)
+  : (S.transform T).vec = T *ᵥ S.vec := rfl
+
 def computeProjection (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) : LinearSystem 𝔽 n :=
   let N : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c < 0}
   let Z : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c = 0}
@@ -48,7 +60,7 @@ def computeProjection (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) : LinearSys
     | .inr (s, t) => (S.mat t ⬝ᵥ c) • S.vec s - (S.mat s ⬝ᵥ c) • S.vec t
   of D d
 
-theorem projectionMatrix_positive {S : LinearSystem 𝔽 n} {c : Fin n → 𝔽}
+theorem projectionMatrix_nonneg {S : LinearSystem 𝔽 n} {c : Fin n → 𝔽}
   : let U := S.projectionMatrix c
     ∀ i, U i ≥ 0 := by
   unfold projectionMatrix
@@ -144,18 +156,13 @@ theorem computeProjection_mat_ortho {S : LinearSystem 𝔽 n} {c : Fin n →
     rw [mul_comm, sub_self]
 
 def projectionMatrix' (S : LinearSystem 𝔽 n) {m : ℕ} (c : Matrix (Fin (m + 1)) (Fin n) 𝔽)
-  : let N : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c 0 < 0}
-    let Z : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c 0 = 0}
-    let P : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c 0 > 0}
-    let R := Z ⊕ₗ (N ×ₗ P)
-    let r := Fintype.card R
-    Matrix (Fin r) (Fin S.m) 𝔽 :=
+  : (r : ℕ) × Matrix (Fin r) (Fin S.m) 𝔽 :=
   match m with
-  | 0 => S.projectionMatrix (c 0)
-  | n + 1 =>
+  | 0 => ⟨_, S.projectionMatrix (c 0)⟩
+  | _ + 1 =>
     let U := S.projectionMatrix (c 0)
-    let U' := S.projectionMatrix' (vecTail c)
-    U' * U
+    let ⟨_, U'⟩ := S.transform_m _ ▸ (S.transform U).projectionMatrix' (vecTail c)
+    ⟨_, U' * U⟩
 
 end LinearSystem
 

diff --git a/PolyhedralCombinatorics/Projection/FourierMotzkin.lean b/PolyhedralCombinatorics/Projection/FourierMotzkin.lean
@@ -40,6 +40,10 @@ theorem mem_fourierMotzkin  {S : LinearSystem 𝔽 n} {j : Fin n} :
 def fourierMotzkinElim0 (S : LinearSystem 𝔽 (n + 1)) : LinearSystem 𝔽 n :=
   (S.fourierMotzkin 0).elim0
 
+theorem fourierMotzkinElim0_projectionMatrix (S : LinearSystem 𝔽 (n + 1))
+  : ∀ (i : Fin _),
+    (S.projectionMatrix x_[0] * S.mat) i = vecCons 0 (S.fourierMotzkinElim0.mat i) := sorry
+
 theorem mem_fourierMotzkinElim0 {S : LinearSystem 𝔽 (n + 1)} {x : Fin n → 𝔽}
   : x ∈ S.fourierMotzkinElim0.solutions ↔ ∃ x₀ : 𝔽, vecCons x₀ x ∈ S.solutions := by
   unfold fourierMotzkinElim0
@@ -76,4 +80,9 @@ def fourierMotzkinElimRec {n : ℕ} (S : LinearSystem 𝔽 n) : LinearSystem
     . apply ih
     . exact S.fourierMotzkinElim0_eq_empty_iff
 
+@[simp] theorem recElimDimensions_eq_empty_iff_exists_neg (S : LinearSystem 𝔽 n)
+  : S.fourierMotzkinElimRec.solutions = ∅ ↔ ∃ i, S.fourierMotzkinElimRec.vec i < 0 := by
+  simp_rw [solutions, Set.eq_empty_iff_forall_not_mem, Set.mem_setOf, mulVec_empty, forall_const,
+    Pi.le_def, not_forall, Pi.zero_apply, not_le]
+
 end LinearSystem