Using the Proof assistant for probability and learning theory? How to get started?

Using Coq
2

There is already some work in Coq to formalize various aspects of and results in machine learning:

http://ace.cs.ohio.edu/~gstewart/papers/aaai19-bagnall.pdf

Also for related systems: https://dl.acm.org/doi/10.5555/3305890.3305996

There are indeed several real number constructions, see for example:
https://coq.inria.fr/distrib/V8.11.0/stdlib/Coq.Reals.ClassicalDedekindReals.html
https://coq.inria.fr/distrib/V8.11.0/stdlib/Coq.Reals.ConstructiveCauchyReals.html

See the topic on probability theory for more about that: (Finite, discrete) Probabilities in Coq?