Email Gateway (Aug 22 2022 at 13:01): Email Gateway (Aug 22 2022 at 13:01):From: Mark Wassell <mpwassell@gmail.com>
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
Email Gateway (Aug 22 2022 at 13:02):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Last updated: Apr 19 2024 at 08:19 UTC