Re: [isabelle] Integration by substitution



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

 - Johannes



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
> was
> proven for the gauge integral (or some special cases) in the
> multivariate
> analysis library.
> Best,
> Mohammad




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.