How to prove in Mathematica

Exploot project

Ivan Cnop
Vrije universiteit Brussel
icnop@vub.ac.be

The fundamental theorem of calculus

The statement

Clear[f];

D[Integrate[f[t], {t, a, x}], x]

((∂((∫_a^x) f(
                  t) \[DifferentialD]t))/(∂x))

Mathematica knows this theorem. 
The condition that    f  should be continuous has to be checked each time we input a particular   f  .

This may generate some warnings.

Integrate[1/ t, {t, -1, 2}]

D[Integrate[1/t, {t, 0, x}], x]

In some cases this may lead to generalised functions:

Integrate[1/t, {t, -1, x}]

D[%, x]

Plot[UnitStep[t] -  .2, {t, -1, 1}]

Integrate[UnitStep[t], {t, -1, x}]

D[%, x]

We will not go into these advanced topics.

Example

Integrate[(t^3) - 3 t + 3, {t, a, x}]

D[%, x]

% /. x -> t

Motivation

Run the following animation to see what can be expected

<< Graphics`FilledPlot`

g[x_] := 
      Which[x < 1, (x^3) - 3 x + 3, x > 1, 0]
h[x_] := Which[x < 1, 0, x > 1, (x^3) - 3 x + 3]

Do[FilledPlot[{g[x], h[x]}, {x, -1, 1 + a}, 
        PlotRange -> {{-2, 4}, {-1, 5}}], {a, 
        1,  .1, - .1}]

In this graph,   x  is  1  and   h  is some small positive number.

Proof

The following simplification is not yet built-in in Mathematica:

(∫_a^(x + h))f[t] \[DifferentialD]t - (∫_a^x) f[
            t] \[DifferentialD]t

but it can be formulated as a rule

\(rule = \((∫\_c_\%b_ f_[
                  t] \[DifferentialD]t - ∫\_c_\%a_ f_[
                  t] \[DifferentialD]t -> ∫\_a\%b f_[
                t] \[DifferentialD]t)\)\)

(∫_0^(x + h))f[t] \[DifferentialD]t - (∫_0^x) f[
              t] \[DifferentialD]t /. rule

Now use a fact about integrals. This expression is   h   times the value of  f  somewhere in the integration interval around x . After division by   h   this value will be close to   f(x)   if the function is continuous. Therefore the limit is  f(x)  as  h   goes to  0 .

Conclusion

Proving is possible in a computer algebra system if the appropriate rules are given.