Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Integral in Isabelle


view this post on Zulip Email Gateway (Aug 22 2022 at 13:05):

From: Omar Jasim <oajasim1@sheffield.ac.uk>
Hi

Please I have to use integration from 0 to infinity for a function as
bellow:

u = (sqrt (∫ (0 -> inf). x(t)^2 dt)) < inf for all t and x(t) is
element in a set.

I tried to find integration in the theories and I found:
"Interval_Integral" and "Set_Integral".

but there are alot of lemmas so please which one is more suitable for this
case?

Regards
Omar


Last updated: Apr 25 2024 at 20:15 UTC