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?
