Since it seems nobody on list knows, you might like to ask the original
authors of the theories about integrals, whose details are written at the
top of src/real/integralScript.sml (copied below):
Theory: GAUGE INTEGRALS
Description: Generalized gauge intgrals and related theorems
(ported from the HOL Light theory of the same)
Email: grace_...@163.com
DATE: 08-10-2012
Ported by:
Weiqing Gu, Zhiping Shi, Yong Guan, Shengzhen Jin, Xiaojuan Li
Beijing Engineering Research Center of High Reliable Embedded System
College of Information Engineering, Capital Normal University (CNU)
Beijing, China
On Sat, Feb 1, 2014 at 10:59 AM, yefengleng <yefengl...@gmail.com> wrote:
> Thank you for your reply, I have not figure this problem. Could you
> explain it in some detail?
>
>
> 2014-01-31 Ramana Kumar <ram...@member.fsf.org>:
>
> Did you figure this problem out? It looks like there aren't any
>> experts on using the integral theories on this list at the moment,
>> unfortunately...
>>
>> On Sun, Dec 15, 2013 at 8:28 AM, 赵刚 <yefengl...@gmail.com> wrote:
>> > Thank you for your reply！I want to prove this
>> > g`! f:real->real a:real !b:real. &0 <= a /\ &0 <= b /\ integrable
>> (&0,b) f
>> > ==> (integral(&0,a)(\y. integral(&0,y)(\x.f x * y ) ) =
>> integral(&0,a)(\y.
>> > integral(&0,y)(\x.f x)* y ))`;
>> > the problem is this proof needs condition "&0 <= y", but I can't proof
>> it
>> > from "\y".
>> > can you help me prove it ? Thank you very much!
>> >
>> >
>> > 2013/12/14 Ramana Kumar <ram...@member.fsf.org>
>> >>
>> >> I'm not sure I understand what the problem is. Perhaps you could show
>> >> us something that you want to prove but cannot prove?
>> >> The term you showed looks fine to me for a double integral.
>> >> It doesn't matter if "x" in "(\x. f x * y) : real -> real" is
>> >> unbounded, because "integral (a,b)" puts the bounds on.
>> >>
>> >> On Mon, Dec 9, 2013 at 10:28 AM, 赵刚 <yefengl...@gmail.com> wrote:
>> >> > I just want to define a Double integral like "integral (c,d)(\y.
>> >> > integral(a,b)(\x. f x * y))"
>> >> > this define just can do on HOL4, but can't compute the internal
>> >> > integral,because the \x. belong to from negative infinity to positive
>> >> > infinity,but the variable of internal integral just belong to (a,b).
>> So
>> >> > it's
>> >> > not equal,someone can help me ~very thanks!
>> >> >
>> >> >
>> >> >
>> >> >
>> ------------------------------------------------------------------------------
>> >> > Rapidly troubleshoot problems before they affect your business. Most
>> IT
>> >> > organizations don't have a clear picture of how application
>> performance
>> >> > affects their revenue. With AppDynamics, you get 100% visibility into
>> >> > your
>> >> > Java,.NET, & PHP application. Start your 15-day FREE TRIAL of
>> >> > AppDynamics
>> >> > Pro!
>> >> >
>> >> >
>> http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
>> >> > _______________________________________________
>> >> > hol-info mailing list
>> >> > hol-info@lists.sourceforge.net
>> >> > https://lists.sourceforge.net/lists/listinfo/hol-info
>> >> >
>> >
>> >
>> >
>> >
>> > --
>> > 赵刚
>>
>
>
------------------------------------------------------------------------------
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121051231&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
