Add matrix definitions and utility functions for probabilistic operations

Author: HEIGE-PCloud

ProgramAnalysis/ProbabilisticPrograms/Example.lean

@@ -1,7 +1,14 @@
 import Mathlib.Data.Matrix.Basic
+import Mathlib.Data.Matrix.Basis
 
 def matrix1 : Matrix (Fin 2) (Fin 3) Nat := ![![1, 2, 3], ![4, 5, 6]]
 def matrix2 : Matrix (Fin 3) (Fin 2) Nat := ![![1, 2], ![3, 4], ![5, 6]]
 
 #eval matrix1
 #eval matrix1 * matrix2
+
+
+def matrix3 : Matrix (Fin 11) (Fin 11) Nat := 0
+
+def manualBasisMatrix (row col : Fin 3) : Matrix (Fin 3) (Fin 3) Nat :=
+  fun i j => if i = row ∧ j = col then 1 else 0

ProgramAnalysis/ProbabilisticPrograms/PWhile.lean

@@ -1,5 +1,7 @@
 module
 public import Lean
+public import Mathlib.Data.Matrix.Basic
+public import Mathlib.Data.Finset.Basic
 
 namespace ProgramAnalysis.ProbabilisticPrograms
 
@@ -371,6 +373,14 @@ def Stmt.size : Stmt → Nat
   | .sif _ _ s1 s2 => s1.size + s2.size + 1
   | .swhile _ _ s => s.size + 1
 
+def E (size : Nat) (row col : Fin size) : Matrix (Fin size) (Fin size) (Fin 2) :=
+  fun i j => if i = row ∧ j = col then 1 else 0
+
+def U (s : Finset Nat) (f : s → s) : Matrix s s (Fin 2) :=
+  fun i j => if f i = j then 1 else 0
+
+def P (s : Finset Nat) (f : s → Bool) : Matrix s s (Fin 2) :=
+  fun i j => if i = j ∧ f i then 1 else 0
 
 
 end ProgramAnalysis.ProbabilisticPrograms