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 > ------------------------------------------------------------------------------ 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
