Re: [isabelle] Improper Integrals in Isabelle



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
> 




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