Computing a well-known improper integral

Today, I wish to show how to prove the computation of a well-known integral. I am using Coquelicot 2.1.1. The integral is as follows and
m is positive.

$\displaystyle \int_{-\infty}^{+\infty} \frac{1}{m} \frac{{\rm d}x}{\frac{x}{m^2} + 1} = \pi$

There is a lemma named is_RInt_derive with the following statement:

forall (f df : R -> R) (a b : R),
(forall x : R, Rmin a b <= x <= Rmax a b -> is_derive f x (df x)) ->
(forall x : R, Rmin a b <= x <= Rmax a b -> continuous df x) ->
is_RInt df a b (f b - f a)

So we should be able to use the fact that the library already contains facts about the derivative of the arctangent function.

We start the proof with the following statement.

Lemma integral_atan_comp_scal m : 0 < m ->
   is_RInt_gen (fun x => /m * /((x / m) ^ 2 + 1)) 
       (Rbar_locally m_infty) (Rbar_locally p_infty) PI.
Proof.
intros m0.

In this statement, the name is_RInt_gen means the sentence the improper integral of the given function between the given bounds is defined and has the given value. Here the given function is

$\displaystyle x\mapsto \frac{1}{m}\frac{1}{{\frac{x}{m}}^2 + 1}$

The bounds are not given as points in R, nor in R-bar, but as limits: this is where the integral is improper.

Then we want to use directly the derivation property, so we show this derivation explicitely:

assert (is_derive_atan_scal : forall x,  
           is_derive (fun x => atan (x / m)) x (/ m * /((x/m)^2 + 1))).

This can be proved quite fast, thanks to the tactic provided in coquelicot, called auto_derive

intros x; auto_deriv.

This generates the following goals.

  m : R
  m0 : 0 < m
  x : R_AbsRing
  ============================
   True

subgoal 2 (ID 471) is:
 1 * / m * / (1 + x * / m * (x * / m * 1)) = / m * / ((x / m) ^ 2 + 1)

The first goal is proved by auto (and I have yet to understand why this goal is not discarded by the tactic), the second goal is proved by field, but not completely, because this tactics requires that we verify that denominators are non zero.

Dealing with the improper integral itself

That an improper integral converges means that for every pairs of real numbers a and b approaching the bounds, the proper integral between a and b converges to a value, and this value has a limit when a and b tend to the bounds. To establish this, we will exhibit a mathematical function and show that this function has the limit we want. In our case, the function is:

$(a,b) \mapsto atan (b/m) - atan (a/m)$

Stating that we will use this function is done simply by using the exists tactic. The definition of is_RInt_gen then imposes that we show first that this function coincides with integrals at arbitrary bounds and second that this function has the right limit. The first part is expressed using a filterprod instance, because we only need this function to describe proper integrals when we get close to the bounds. As we explained at the beginning of this article, the theorem is_RInt_derive require a proof that the derivative is continuous. This imposes that we prove that the integrand is continuous. This can be done automatically, because this function is actually derivable, and we already have automatic tactic auto_derive to deal with proving the derivability of functions. So we rely on the following theorem:

ex_derive_continuous
 : forall (f : ?K -> ?V) (x : ?K), ex_derive f x -> continuous f x

This theorem turns out to be slightly more complex to use than expected because the implicit arguments are not inferred properly by the Coq system, for a reason I don’t understand. In practice, I have the goal:

============================
forall x : R,
Rmin u v <= x <= Rmax u v ->
continuous (fun x0 : R => / m * / (x0 / m * (x0 / m * 1) + 1)) x

and I need to type the following tactic.

intros x _; apply (@ex_derive_continuous R_AbsRing R_NormedModule).

I guessed the arguments R_AbsRing and R_NormedModule, because the Check command on ex_derive_continuous indicated that the parameter K had to have type AbsRing and the parameter V had to have type NormedModule K.

Once I have transformed the goal into proving that the integrand is derivable, the automatic tactic auto_derive finishes the job almost completely, again generating a side-condition to verify that the denominator is non-zero.

Dealing with the limits

We need to prove that the limit of the function is $\pi$ . This expressed with the following goal.

============================
   filterlim (fun p : R * R => atan (snd p / m) - atan (fst p / m))
     (filter_prod (Rbar_locally m_infty) (Rbar_locally p_infty)) 
     (locally PI)

Here the predicate filterlim establishes a relation between an input filter (which describes the simultaneous limits
of two inputs towards minus infinity and plus infinity, respectively) and an output filter (which describes the limit towards $\pi$ .

My first attempt works by going back to traditional $\displaystyle \varepsilon-\delta$ reasoning. This is not the right way to do, but I can’t help showing it. The first step is to make an $\displaystyle \varepsilon$ appear. The filter locally PI means that we need to consider
all sets around $\pi$ , so we can introduce an arbitrary set and the property that this set is around $\pi$ is expressed by the existence of a given $\varepsilon$ (named ep) in my formal proof), so I can introduce all of them in the following manner.

intros S HS; destruct HS as [ep Pep].

And the resulting goal has the following shape.

  S : R_NormedModule -> Prop
  ep : posreal
  Pep : forall y : R_NormedModule, ball PI ep y -> S y
  ============================
   filtermap (fun p : R * R => atan (snd p / m) - atan (fst p / m))
     (filter_prod (Rbar_locally m_infty) (Rbar_locally p_infty)) S

Here the predicate filtermap lifts a function into a relation between a filter and a set. This actually requires that we express that the filter will contain sets whose image by the function is guaranteed to be in S. In this case, we will be
stronger and guarantee that the image is in the ball centered in $\pi$ with radius $\varepsilon$ .

If $\varepsilon$ is small enough, we know that a good way to approach $\displaystyle \frac{\pi}{2}$ through the function $\displaystyle atan \frac{x}{m}$ is to take values larger than $\displaystyle m \times \tan \frac{\pi - \varepsilon}{2}$ in absolute value. But for now, $\varepsilon$ is not guaranteed to be small enough, so we choose to take another value which is the minimum of $\varepsilon$ and $\pi$ .

Leave a Reply Cancel reply