For a nondecreasing right-continuous function , the Lebesgue-Stieltjes measure associated is formalized as interval_measure
in the theory Lebesgue_Measure
. However, I cannot find a well-known formula
(when and satisfy some appropriate conditions). Is this already formalized in Isabelle_HOL
?
This probably belongs in #Is there code for X?
Thank you very much for the reply.
Do you mean this entry?
https://devel.isa-afp.org/entries/Bernoulli.html
You might want to look into Change_Of_Vars.thy, looks like theorem cov_invertible_real is similar to what you're looking for
Thank you very much for the comment.
It looks similar as you say, but unfortunately the lemmas such as cov_invertible_real
seem different from what I want.
They tell about the Lebesgue measure, but I need the lemma of Lebesgue-Stieltjes measure (interval_measure
in Isabelle).
If you could find me a text proof for the above theorem then I'd be happy to try and mechanise it
I really appreciate your help!
However, I have not been able to find a precise proof of this lemma...
The closest one seems to be
"7.3.5 Absolutely continuous functions and absolutely continuous measures" (p.39) in
https://www.uab.edu/cas/mathematics/images/Documents/reals.pdf
This only contains the sketch of the proof.
Simultaneously, Larry Paulson send me an email. He said that, if he could get a rigorous paper proof, he would check HOL light. I replied to him and sent the link above, but I haven't got a reply.
So I think I have to make a precise paper proof by myself before formalizing it...
I'm afraid that after searching myself I find a number of slightly different versions of the theorem, and no mechanisable proofs. Very odd indeed.
Thank you again for your help.
I thought that the formula was well-known, but, after knowing your search result, maybe my understanding was wrong. This formula may be "domain-specific", though it is indispensable to calculating the Lebesgue-Stieltjes integral in actuarial mathematics.
I have found that the lemma nn_integral_density
in the theory Nonnegative_Lebesgue_Integration
in HOL-Analysis is sufficient for my application.
I should have noticed it earlier. Thank you all for your comments.
Last updated: Jan 05 2025 at 20:18 UTC