Revision history [back]

Attempting to derive the cdf of the normal distribution from its pdf.

http://en.wikipedia.org/wiki/Normal_distribution

sage: var('x mu sigma')
sage: PDF = function('PDF', x, mu, sigma)
sage: normal = (PDF == 1/(sigma * sqrt(2 * pi))*e^(-(x - mu)^2/(2*sigma^2)))
sage: normal

$\newcommand{\Bold}[1]{\mathbf{#1}}{\rm PDF}\left(x, \mu, \sigma\right) = \frac{\sqrt{2} e^{\left(-\frac{{\left(\mu - x\right)}^{2}}{2 \, \sigma^{2}}\right)}}{2 \, \sqrt{\pi} \sigma}$

sage: eq1 = integrate(normal, x) 
sage: eq1

$\newcommand{\Bold}[1]{\mathbf{#1}}\int {\rm PDF}\left(x, \mu, \sigma\right)\,{d x} = c_{2} + \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right)$

I happen to know that c2 should be 1/2, but don't see a way to give sage enough information to prove it out.

This isn't my main difficulty however. I'll just substitute it manually for now...

sage: eq1 = eq1.substitute(c2 = 1/2)
sage: eq1

$\newcommand{\Bold}[1]{\mathbf{#1}}\int {\rm PDF}\left(x, \mu, \sigma\right)\,{d x} = \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2}$

This is the solution found on wikipedia:

sage: eq2 = integrate(PDF, x) == 1/2 * (1 + erf((x - mu)/(sigma * sqrt(2))))
sage: eq2

$\newcommand{\Bold}[1]{\mathbf{#1}}\int {\rm PDF}\left(x, \mu, \sigma\right)\,{d x} = \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right) + \frac{1}{2}$

I'd like to prove that the solution given by sage is the same as given by wikipedia (rather than eyeballing it).

sage: equality = (eq1.right() == eq2.right())
sage: equality

$\newcommand{\Bold}[1]{\mathbf{#1}}\frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2} = \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2}$

I believe this equation is trivially True, but I'd like sage to tell me that.

The simplify() function doesn't help me do it:

sage: simplify(equality)

$\newcommand{\Bold}[1]{\mathbf{#1}}\frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2} = -\frac{1}{2} \, \text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2}$

solve(,x) does however get me significantly closer:

sage: equality = solve(equality, x)[0]
sage: equality

$\newcommand{\Bold}[1]{\mathbf{#1}}\text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = \text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right)$

The forms on both sides are exactly the same, can't sage reduce this directly to True from here?

The next step in the solution would be to inverse-erf both sides of the equation.

How come sage doesn't know that? How can I tell it?

I'll try to force it by running the inverse-erf function on the equation.
I couldn't find such a function, but I can get sage to give me one:

sage: var('x y')
sage: inverse_erf = solve(erf(x) == y, x)
sage: inverse_erf

$\newcommand{\Bold}[1]{\mathbf{#1}}\left[x = {\rm inverse}_{{\rm erf}}\left(y\right)\right]$

sage: inverse_erf = inverse_erf[0].right().operator()
sage: inverse_erf

$\newcommand{\Bold}[1]{\mathbf{#1}}inverse_erf$

This doesn't work the way I had hoped...

Why doesn't the `inverse_erf()` function distribute itself across the equation?

sage: inverse_erf(equality)

$\newcommand{\Bold}[1]{\mathbf{#1}}{\rm inverse}_{{\rm erf}}\left(\text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = \text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right)\right)$

It doesn't even work in the most basic case, so maybe I've completely gone off the rails?

sage: simplify(inverse_erf(erf(x)))

$\newcommand{\Bold}[1]{\mathbf{#1}}{\rm inverse}_{{\rm erf}}\left(\text{erf}\left(x\right)\right)$

In summary: What have I done wrong, and how can I do it better?

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf(sqrt(2)*mu - sqrt(2)*x) == -erf(sqrt(2)*(mu - x)))
sage: show(eq3)
sage: show(bool(eq3))
sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

Attempting to derive the cdf of the normal distribution from its pdf.

http://en.wikipedia.org/wiki/Normal_distribution

sage: var('x mu sigma')
sage: PDF = function('PDF', x, mu, sigma)
sage: normal = (PDF == 1/(sigma * sqrt(2 * pi))*e^(-(x - mu)^2/(2*sigma^2)))
sage: normal

$\newcommand{\Bold}[1]{\mathbf{#1}}{\rm PDF}\left(x, \mu, \sigma\right) = \frac{\sqrt{2} e^{\left(-\frac{{\left(\mu - x\right)}^{2}}{2 \, \sigma^{2}}\right)}}{2 \, \sqrt{\pi} \sigma}$

sage: eq1 = integrate(normal, x) 
sage: eq1

$\newcommand{\Bold}[1]{\mathbf{#1}}\int {\rm PDF}\left(x, \mu, \sigma\right)\,{d x} = c_{2} + \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right)$

I happen to know that c2 should be 1/2, but don't see a way to give sage enough information to prove it out.

This isn't my main difficulty however. I'll just substitute it manually for now...

sage: eq1 = eq1.substitute(c2 = 1/2)
sage: eq1

$\newcommand{\Bold}[1]{\mathbf{#1}}\int {\rm PDF}\left(x, \mu, \sigma\right)\,{d x} = \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2}$

This is the solution found on wikipedia:

sage: eq2 = integrate(PDF, x) == 1/2 * (1 + erf((x - mu)/(sigma * sqrt(2))))
sage: eq2

$\newcommand{\Bold}[1]{\mathbf{#1}}\int {\rm PDF}\left(x, \mu, \sigma\right)\,{d x} = \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right) + \frac{1}{2}$

I'd like to prove that the solution given by sage is the same as given by wikipedia (rather than eyeballing it).

sage: equality = (eq1.right() == eq2.right())
sage: equality

$\newcommand{\Bold}[1]{\mathbf{#1}}\frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2} = \frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2}$

I believe this equation is trivially True, but I'd like sage to tell me that.

The simplify() function doesn't help me do it:

sage: simplify(equality)

$\newcommand{\Bold}[1]{\mathbf{#1}}\frac{1}{2} \, \text{erf}\left(-\frac{\sqrt{2} \mu}{2 \, \sigma} + \frac{\sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2} = -\frac{1}{2} \, \text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) + \frac{1}{2}$

solve(,x) does however get me significantly closer:

sage: equality = solve(equality, x)[0]
sage: equality

$\newcommand{\Bold}[1]{\mathbf{#1}}\text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = \text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right)$

The forms on both sides are exactly the same, can't sage reduce this directly to True from here?

The next step in the solution would be to inverse-erf both sides of the equation.

How come sage doesn't know that? How can I tell it?

I'll try to force it by running the inverse-erf function on the equation.
I couldn't find such a function, but I can get sage to give me one:

sage: var('x y')
sage: inverse_erf = solve(erf(x) == y, x)
sage: inverse_erf

$\newcommand{\Bold}[1]{\mathbf{#1}}\left[x = {\rm inverse}_{{\rm erf}}\left(y\right)\right]$

sage: inverse_erf = inverse_erf[0].right().operator()
sage: inverse_erf

$\newcommand{\Bold}[1]{\mathbf{#1}}inverse_erf$

This doesn't work the way I had hoped...

Why doesn't the `inverse_erf()` function distribute itself across the equation?

sage: inverse_erf(equality)

$\newcommand{\Bold}[1]{\mathbf{#1}}{\rm inverse}_{{\rm erf}}\left(\text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = \text{erf}\left(-\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right)\right)$

It doesn't even work in the most basic case, so maybe I've completely gone off the rails?

sage: simplify(inverse_erf(erf(x)))

$\newcommand{\Bold}[1]{\mathbf{#1}}{\rm inverse}_{{\rm erf}}\left(\text{erf}\left(x\right)\right)$

In summary: What have I done wrong, and how can I do it better?

I used @ndomes' method of using numeric functions, which solved my 1/2 issue above, but I still wind up unable to prove that erf... == erf.... What's going on here??

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf(sqrt(2)*mu - sqrt(2)*x) == -erf(sqrt(2)*(mu - x)))
sage: show(eq3)
sage: show(bool(eq3))
sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\sqrt{2} \mu - \sqrt{2} x\right) = -\text{erf}\left(\sqrt{2} {\left(\mu - x\right)}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{True}$

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{False}$

sage: var('x mu sigma')
sage: PDF = function('PDF', x, mu, sigma)
sage: normal = (PDF == 1/(sigma * sqrt(2 * pi))*e^(-(x - mu)^2/(2*sigma^2)))
sage: normal

sage: eq1 = integrate(normal, x) 
sage: eq1

sage: eq1 = eq1.substitute(c2 = 1/2)
sage: eq1

sage: eq2 = integrate(PDF, x) == 1/2 * (1 + erf((x - mu)/(sigma * sqrt(2))))
sage: eq2

sage: equality = (eq1.right() == eq2.right())
sage: equality

sage: simplify(equality)

sage: equality = solve(equality, x)[0]
sage: equality

sage: var('x y')
sage: inverse_erf = solve(erf(x) == y, x)
sage: inverse_erf

sage: inverse_erf = inverse_erf[0].right().operator()
sage: inverse_erf

sage: inverse_erf(equality)

sage: simplify(inverse_erf(erf(x)))

I used @ndomes' method of using numeric functions, but I still wind up unable to prove that erf... == erf.... What's going on here??:

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf(sqrt(2)*mu - sqrt(2)*x) == -erf(sqrt(2)*(mu - x)))
sage: show(eq3)
sage: show(bool(eq3))
sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\sqrt{2} \mu - \sqrt{2} x\right) = -\text{erf}\left(\sqrt{2} {\left(\mu - x\right)}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{True}$

sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{False}$

sage: solve(erf(x) == erf(y), x)[0].simplify_full()
x == inverse_erf(erf(y))

I used @ndomes' method of using numeric functions, but I still wind up unable to prove that erf... == erf...:

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf(sqrt(2)*mu - sqrt(2)*x) == -erf(sqrt(2)*(mu - x)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\sqrt{2} \mu - \sqrt{2} x\right) = -\text{erf}\left(\sqrt{2} {\left(\mu - x\right)}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{True}$

sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{False}$

What's going on here?? Is it related to being unable to reduce inverse_erf(erf()) below?

sage: solve(erf(x) == erf(y), x)[0].simplify_full()
x == inverse_erf(erf(y))

I used @ndomes' method of using numeric functions, but I still wind up unable to prove that erf... == erf...:

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf(sqrt(2)*mu - sqrt(2)*x) == -erf(sqrt(2)*(mu - x)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\sqrt{2} \mu - \sqrt{2} x\right) = -\text{erf}\left(\sqrt{2} {\left(\mu - x\right)}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{True}$

sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{False}$

This slightly simpler equation works correctly however:

sage: eq4 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(sigma)) == -erf((sqrt(2)*(mu - x))/(sigma)))
sage: show(eq4)
sage: show(bool(eq4))

$-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{\sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{\sigma}\right)$

$\mathrm{True}$

What's going on here?? Is it related to being unable to reduce inverse_erf(erf()) below?

sage: solve(erf(x) == erf(y), x)[0].simplify_full()
x == inverse_erf(erf(y))

I used @ndomes' method of using numeric functions, but I still wind up unable to prove that erf... == erf...:

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{False}$

This slightly simpler equation works correctly however:

sage: eq4 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(sigma)) == -erf((sqrt(2)*(mu - x))/(sigma)))
sage: show(eq4)
sage: show(bool(eq4))

$-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{\sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{\sigma}\right)$

$\mathrm{True}$

What's going on here?? Is it related to being unable to reduce inverse_erf(erf()) below?

sage: solve(erf(x) == erf(y), x)[0].simplify_full()
x == inverse_erf(erf(y))

I used @ndomes' method of using numeric functions, but I still wind up unable to prove that erf... == erf...:

sage: var('x sigma mu')
sage: assume(sigma > 0)
sage: eq3 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(2*sigma)) == -erf((sqrt(2)*(mu - x))/(2*sigma)))
sage: show(eq3)
sage: show(bool(eq3))

$\newcommand{\Bold}[1]{\mathbf{#1}}-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{2 \, \sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{2 \, \sigma}\right)$

$\newcommand{\Bold}[1]{\mathbf{#1}}\mathrm{False}$

This slightly simpler equation works correctly however:

sage: eq4 = (-erf((sqrt(2)*mu - sqrt(2)*x)/(sigma)) == -erf((sqrt(2)*(mu - x))/(sigma)))
sage: show(eq4)
sage: show(bool(eq4))

$-\text{erf}\left(\frac{\sqrt{2} \mu - \sqrt{2} x}{\sigma}\right) = -\text{erf}\left(\frac{\sqrt{2} {\left(\mu - x\right)}}{\sigma}\right)$

$\mathrm{True}$

What's going on here?? Is it related to being unable to reduce inverse_erf(erf()) below?

sage: solve(erf(x) == erf(y), x)[0].simplify_full()
x == inverse_erf(erf(y))