Radon-Nikodym theorem and constructive mathematics

131 Views Asked by At

I am interested in learning how nonconstructive the proof of the existence of R-N derivative is. I know that there is no general recipe for computing the R-N derivative. It can be explicitly computed if one knows a differentiation basis with the Vitali property. To this extent, it seems the original existence proof is highly nonconstructive. But does anyone know if there is a precise calibration of how nonconstructive the proof is (e.g. is it provable in constructive mathematics? And how it stands in the zoo of reverse mathematics?) Many thanks in advance.