search

gogotanaka / hilbert

:dancers: Implement mathematics.
http://hilbert-lang.org/
553 stars 36 forks source link

Incorrect answers for improper integrals #75

Open jackmaney opened 9 years ago

jackmaney commented 9 years ago 
Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(x dx)[-oo..oo]
0.0
Enjoy! ->

Since S(x dx)[-oo..oo] is improper at both endpoints (and the integrand has no discontinuities), the correct way to evaluate this integral is to split up the interval into two pieces: S(x dx)[-oo..0] + S(x dx)[0..oo]. Neither of these integrals converge, therefore S(x dx)[-oo..oo] diverges as well.

jackmaney commented 9 years ago

In a similar vein, we have this:

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(1/x dx)[-1..1]
oo
Enjoy! ->

This is also incorrect: the integral diverges.

jackmaney commented 9 years ago

Likewise:

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(1/x dx)[1..oo]
6.90916718
Enjoy! ->

The most general antiderivative of 1/x is ln(|x|) + C which, of course, goes to infinity as x goes to infinity.

jackmaney commented 9 years ago

Oh dear...

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(sin(x) dx)[0..oo]
0.43777752000000003
Enjoy! ->
jackmaney commented 9 years ago 
Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(x^(-0.5) dx)[0..1]
oo
jackmaney commented 9 years ago

Here's another wrong one:

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(log(x)/x^(0.5) dx)[0..1]
-oo
jackmaney commented 9 years ago

Here's another:

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> S(1/(1-x^2)^0.5 dx)[0..1]
oo

The correct answer is, of course, Math::PI / 2.