Linear algebra with Eigen

Stream: lean4

[Tomas Skrivan]

If anyone is interested, I have created a proof of concept library binding Eigen c++ library. Right now, it can only solve linear system with Cholesky decomposition or initialize sparse matrix and convert it to dense format, pretty useless on its own :smile: However, adding more capabilities should be relatively straightforward and follow the same pattern. It can also serve as a bit more complicated FFI example.

I do not have immediate plan to grow this library too much, I will be adding functions only as I need them in other projects. But if someone is interested we can coordinate a bit more structured approach.

Example of solving linear system:

  let A : Matrix 2 2 := ⟨FloatArray.mk #[2,1,1,2], by native_decide⟩
  let b : Matrix 2 1 := ⟨FloatArray.mk #[1,1], by native_decide⟩
  IO.println (A.ldlt.solve b)

Prints out [0.333333, 0.333333]

Example of initializing sparse matrix from triples:

  let entries : Array (Triplet 2 2) := (#[(0,0,1.0), (1,1,-1.0), (0,1, 2.0)] : Array (Nat×Nat×Float))
  let B := SparseMatrix.mk entries
  IO.println B.toDense

Prints out [1.000000, 0.000000, 2.000000, -1.000000]