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
