Email Gateway (Aug 22 2022 at 12:02): Email Gateway (Aug 22 2022 at 12:02):From: Mohammad Abdul Aziz <mohammad.abdulaziz8@gmail.com>
Hello All,
I would like to know whether the integration by substitution identity was
proven for the gauge integral (or some special cases) in the multivariate
analysis library.
Best,
Mohammad
Email Gateway (Aug 22 2022 at 12:02):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Mohammad,
it is not directly available for the Gauge integral in Isabelle/HOL.
Luckily, in HOL-Probability is integration by substitution proved for
continuous f, g :: real => real with "interval_integral_substitution"
or "integral_substitution".
(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)
as f and g are continuous the Lebesgue integral and the gauge integral
are equal. This can be proved with "integral_lborel" and
"integrable_on_lborel".
Last updated: Apr 25 2024 at 12:23 UTC