Re: [isabelle] Integration by substitution
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"
(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
Am Montag, den 14.12.2015, 19:06 +0000 schrieb Mohammad Abdul Aziz:
> Hello All,
> I would like to know whether the integration by substitution identity
> proven for the gauge integral (or some special cases) in the
> analysis library.
This archive was generated by a fusion of
Pipermail (Mailman edition) and