Does there exist any work on creating a Real Number/Probability Theory Framework in COQ?
The standard library of Coq has a section about real numbers. These are the classical real numbers, using the Dedekind completion. There are also results about complex numbers, I suppose there are several libraries, I happen to know this one. Note that there is also a lot of results for constructive real and complex numbers, C-CoRN is the reference.

Side note: you could also define (computable) real numbers inductively with some of the constructive axiomatics, for example using rational numbers from the Cauchy sequences or some constructive version of the least-upper-bound property. I am not sure how much inductive that this.

I know there are some people working on probabilities with Coq. Unfortunately I am not sure how advanced their works are. My guess is that there is likely no such specific result about Chernoff bound or union bound. (But it's just a guess)