Guillaume Dubach (Oct 19 2020 at 09:33): Guillaume Dubach (Oct 19 2020 at 09:33):Dear math-comp analysis contributors,
I am a postdoc at IST Austria working in Random Matrix Theory - the study of eigenvalues and eigenvectors of matrices whose entries are random. I discovered Coq recently and I formed the project of formalizing a few classical proofs, beginning with the so-called "Wigner semicircle law", which is considered to be the first important discovery in this area.
To do so, I will certainly need measure theory, linear algebra, complex analysis, and a little bit of combinatorics as well. Advice or suggestions are most welcome!
Karl Palmskog (Oct 19 2020 at 09:37):some pieces of measure theory have been done for MathComp in these projects: https://github.com/jtassarotti/coq-proba https://github.com/affeldt-aist/infotheo
Reynald Affeldt (Oct 19 2020 at 09:39):there are more pieces of measure theory in mathcomp-analysis but it is in a PR :-/
Karl Palmskog (Oct 19 2020 at 09:43):some applied probability theory via Infotheo here that may be relevant (but more of a long shot): https://github.com/certichain/ceramist
Karl Palmskog (Oct 19 2020 at 09:45):we have a general thread here about probability theory in Coq: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166
Marie Kerjean (Oct 19 2020 at 11:25):Guillaume and I know each other already, and I advised him to admit anything he needs in complex analysis and measure theory. I also pointed him to your PR @Reynald Affeldt . Meanwhile this is another motivation to get through complex analysis. I also thought that anything serious in probability theory could interest @Pierre-Yves Strub , but I might be wrong.
Guillaume Dubach (Oct 21 2020 at 09:36):Thank you for these references! It looks like these repositories already contain some useful things. May I ask your opinion about the following (quite recent) work:
https://www.researchgate.net/publication/330431409_Formalizing_Probability_Concepts_in_a_Type_Theory
I wondered if this approach was at all compatible with mathcomp (which is not mentioned). But more fundamentally, I would like to know a correct syntax to work with (general, so possibly continuous) random variables. For instance, has the Central Limit Theorem ever been formalized in Coq?
Karl Palmskog (Oct 21 2020 at 09:48):Central Limit Theorem has not been formalized in Coq to my knowledge, just in Isabelle. From a cursory look at the link, this looks like a workshop-or-below l evel paper (a telltale sign is that there are no references at all to the papers on probability in Coq that existed in 2018, most blatantly ALEA which is from 2007)
Bas Spitters (Oct 21 2020 at 14:30):Haven;t seen that work before. Did anyone contact the author?
Last updated: Apr 20 2024 at 14:01 UTC