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