Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Calculation of Lebesgue-Stieltjes Integral

Email Gateway (Oct 03 2024 at 11:54):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Isabelle users,

For a nondecreasing right-continuous function $F$, the Lebesgue-Stieltjes
measure associated with $F$ is formalized as interval_measure in the
theory Lebesgue_Measure.
However, I cannot find the well-known formula
[image: LINT.png]
(when $F$ and $g$ satisfy some appropriate conditions).
Is this already formalized in Isabelle/HOL or AFP?

Best regards,

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

LINT.png

Email Gateway (Nov 19 2024 at 12:56):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Isabelle users,

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.

Best regards,

2024年10月3日(木) 20:46 伊藤洋介 <glacier345@gmail.com>:

Dear Isabelle users,

For a nondecreasing right-continuous function $F$, the Lebesgue-Stieltjes
measure associated with $F$ is formalized as interval_measure in the
theory Lebesgue_Measure.
However, I cannot find the well-known formula
[image: LINT.png]
(when $F$ and $g$ satisfy some appropriate conditions).
Is this already formalized in Isabelle/HOL or AFP?

Best regards,

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com

LINT.png

Last updated: Feb 05 2025 at 16:23 UTC