# [isabelle] Improper Integrals in Isabelle

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