Place for numeric methods

Stream: mathlib4

[Eureka Zheng]

Any recommendations on where to create files for numeric methods for solving linear equations such as the conjugate gradient method?

[Jz Pan]

I'm not aware a place of mathlib contains numerical analysis, but maybe you will be interested in https://github.com/optsuite/optlib

[Luigi Massacci]

Do you want to to just prove theoretical results, or write actual runnable programs? If the former, you can definitely put it somewhere in the Linear Algebra or Analysis folders depending on what exactly you prove. We have for example Lagrange interpolation, Legendre polynomials, etc, I don't see why what you propose should be any different. If it's the latter case however, indeed Mathlib is currently rather poorly equipped to help you. You could take a look at the SciLean project by @Tomas Skrivan.

[Eureka Zheng]

I would like to theoretically prove something about the algorithms. But I'm wondering that in order to prove something about an algorithm (convergence speed etc.), don't we have to first formulate (i.e. implement) the algorithm itself?

[Jz Pan]

Eureka Zheng said:

we have to first formulate (i.e. implement) the algorithm itself

Yes you need, but it could be noncomputable def.

[Luigi Massacci]

Indeed this is what I meant. If you are fine with your algorithm being written down as having type something like $(n : \N) \to (m : \mathcal{M}_n(\R)) \to (\N \to \mathcal{M}_n(\R))$, and then prove say the sequence converges to $m$, then it will be absolutely be suitable for mathlib, you just won't be able to run it. At least not in the near future.