Stream: Beginner Questions

Topic: Calculation of Lebesgue-Stieltjes Integral


view this post on Zulip Yosuke Ito (Sep 29 2024 at 09:39):

For a nondecreasing right-continuous function FF, the Lebesgue-Stieltjes measure associated FF is formalized as interval_measure in the theory Lebesgue_Measure. However, I cannot find a well-known formula

g(x)dF(x)=g(x)F(x)dx\int g(x) dF(x) = \int g(x) F'(x) dx

(when FF and gg satisfy some appropriate conditions). Is this already formalized in Isabelle_HOL?

view this post on Zulip Jonathan Lindegaard Starup (Oct 31 2024 at 12:52):

This probably belongs in #Is there code for X?

view this post on Zulip Yosuke Ito (Oct 31 2024 at 13:32):

Thank you very much for the reply.
Do you mean this entry?
https://devel.isa-afp.org/entries/Bernoulli.html

view this post on Zulip Christian Pardillo Laursen (Nov 03 2024 at 11:12):

You might want to look into Change_Of_Vars.thy, looks like theorem cov_invertible_real is similar to what you're looking for

view this post on Zulip Yosuke Ito (Nov 03 2024 at 11:45):

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).

view this post on Zulip Christian Pardillo Laursen (Nov 05 2024 at 10:52):

If you could find me a text proof for the above theorem then I'd be happy to try and mechanise it

view this post on Zulip Yosuke Ito (Nov 06 2024 at 13:09):

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.

view this post on Zulip Yosuke Ito (Nov 06 2024 at 13:10):

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.

view this post on Zulip Yosuke Ito (Nov 06 2024 at 13:10):

So I think I have to make a precise paper proof by myself before formalizing it...

view this post on Zulip Christian Pardillo Laursen (Nov 08 2024 at 13:41):

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.

view this post on Zulip Yosuke Ito (Nov 09 2024 at 05:41):

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.

view this post on Zulip Yosuke Ito (Nov 19 2024 at 12:46):

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