*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Improper Integrals in Isabelle*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Mon, 21 Mar 2016 11:14:34 +0100*In-reply-to*: <56EBD620.5090803@gmail.com>*Organization*: TU München*References*: <56EBD620.5090803@gmail.com>

Hi Mark, if you want to do 'naive' integration (i.e. Lebesgue integration: your function's upper and lower halfs are integrable) then the HK-integral in HOL-MV_A is not the only integral we have. In HOL-Probability (~~/src/HOL/Probability) there is also the Lebesgue integral and the Bochner integral. Especially, the theory Interval_Integral contains a lot of stuff to relate improper and proper integrals also in with a FTC. As far as I know there is not much for relating the improper and proper integral of the Heinstock-Kurzweil integral in HOL-MV_A. Of course, you need to add the necessary integrability and boundedness assumptions to prove your goals. Also, it maight be easier to replace at_top by sequentially: sequentially allows you to directly use dominated convergence with at_top you need to fiddle around with the limits. - Johannes Am Freitag, den 18.03.2016, 10:19 +0000 schrieb Mark Wassell: > Hello, > > Within the Multivariate_Analysis library, I would like to make use of > the fundamental theorem of calculus to prove theorems about the > values > of improper integrals > (to be exact integrals where the integral is over {a..}, {..b} or > UNIV > for some a and b (which will often be 0)) > > I think I will need to prove something like the following: > > lemma integral_improper_at_top: > fixes f::"real â real" and a::real > shows "integral {a..} f = Lim at_top (ÎL. integral {a..L} f)" > sorry > > and > > lemma fct_improper_at_top: > fixes F::"real â real" and f::"real â real" and a::real > assumes "(F has_vector_derivative (f x)) (at x within {a..})" > shows "integral {a..} f = Lim at_top (ÎL. F(L) - F(a))" > sorry > > Am I on the right track here or is there something else that I can > use? > > Cheers > > Mark >

**References**:**[isabelle] Improper Integrals in Isabelle***From:*Mark Wassell

- Previous by Date: Re: [isabelle] difficulty with a tutorial example
- Next by Date: [isabelle] Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 9th
- Previous by Thread: [isabelle] Improper Integrals in Isabelle
- Next by Thread: [isabelle] PhD and Post-Doc positions at Chalmers
- Cl-isabelle-users March 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list