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 >> > > > > > > -- > 赵刚 ------------------------------------------------------------------------------ WatchGuard Dimension instantly turns raw network data into actionable security intelligence. It gives you real-time visual feedback on key security issues and trends. Skip the complicated setup - simply import a virtual appliance and go from zero to informed in seconds. http://pubads.g.doubleclick.net/gampad/clk?id=123612991&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
