[isabelle] Improper Integrals in Isabelle


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


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

Am I on the right track here or is there something else that I can use?



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