Dear all,
I am working in HOL Light and I want to prove the following theorem
regarding integral:
*!b. f absolutely_integrable_on interval [lift a,lift b] ==> (?k.
((\b. real_integral (real_interval [a,b]) (\t. norm (f (lift t)))) - - ->
k) at_posinfinity)*
which says that if a function is absolutely integrable on [a, infinity),
i.e., the norm of function f is convergent then integral of fucntion's norm
over the same interval approaches to some limit value k which is actually
true.
Can anyone guide me in its proof?
Thanks.
Adnan Rashid
PhD Candidate,
NUST-SEECS,
Islamabad, Pakistan
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
