{"id":91,"date":"2016-09-02T14:24:55","date_gmt":"2016-09-02T12:24:55","guid":{"rendered":"http:\/\/project.inria.fr\/coqexchange\/?p=91"},"modified":"2016-09-02T14:24:55","modified_gmt":"2016-09-02T12:24:55","slug":"computing-a-well-known-improper-integral","status":"publish","type":"post","link":"https:\/\/project.inria.fr\/coqexchange\/computing-a-well-known-improper-integral\/","title":{"rendered":"Computing a well-known improper integral"},"content":{"rendered":"

Today, I wish to show how to prove the computation of a well-known integral.\u00a0 I am using Coquelicot<\/a> 2.1.1. The integral is as follows and
\nm is positive.<\/p>\n\\(\\displaystyle \\int_{-\\infty}^{+\\infty} \\frac{1}{m} \\frac{{\\rm d}x}{\\frac{x}{m^2} + 1} = \\pi\\)\n

There is a lemma named is_RInt_derive<\/tt> with the following statement:<\/p>\n

forall (f df : R -> R) (a b : R),\r\n(forall x : R, Rmin a b <= x <= Rmax a b -> is_derive f x (df x)) ->\r\n(forall x : R, Rmin a b <= x <= Rmax a b -> continuous df x) ->\r\nis_RInt df a b (f b - f a)\r\n<\/pre>\n
So we should be able to use the fact that the library already contains facts about the derivative of the arctangent function.<\/p>\n
We start the proof with the following statement.<\/p>\n
Lemma integral_atan_comp_scal m : 0 < m ->\r\n   is_RInt_gen (fun x => \/m * \/((x \/ m) ^ 2 + 1)) \r\n       (Rbar_locally m_infty) (Rbar_locally p_infty) PI.\r\nProof.\r\nintros m0.\r\n<\/pre>\n
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<\/i>. Here the given function is<\/p>\n\\(\\displaystyle x\\mapsto \\frac{1}{m}\\frac{1}{{\\frac{x}{m}}^2 + 1}\\)\n
The bounds are not given as points in R, nor in R-bar, but as limits: this is where the integral is improper.<\/p>\n
Then we want to use directly the derivation property, so we show this derivation explicitely:<\/p>\n
assert (is_derive_atan_scal : forall x,  \r\n           is_derive (fun x => atan (x \/ m)) x (\/ m * \/((x\/m)^2 + 1))).\r\n<\/pre>\n
This can be proved quite fast, thanks to the tactic provided in coquelicot, called auto_derive<\/tt><\/p>\n
intros x; auto_deriv.\r\n<\/pre>\n
This generates the following goals.<\/p>\n
  m : R\r\n  m0 : 0 < m\r\n  x : R_AbsRing\r\n  ============================\r\n   True\r\n\r\nsubgoal 2 (ID 471) is:\r\n 1 * \/ m * \/ (1 + x * \/ m * (x * \/ m * 1)) = \/ m * \/ ((x \/ m) ^ 2 + 1)\r\n<\/pre>\n
The first goal is proved by auto<\/tt> (and I have yet to understand why this goal is not discarded by the tactic), the second goal is proved by field<\/tt>, but not completely, because this tactics requires that we verify that denominators are non zero.<\/p>\n
Dealing with the improper integral itself<\/strong><\/p>\n
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.\u00a0 To establish this, we will exhibit a mathematical function and show that this function has the limit we want.\u00a0 In our case, the function is:<\/p>\n\\((a,b) \\mapsto atan (b\/m) – atan (a\/m)\\)\n
Stating that we will use this function is done simply by using the exists<\/tt> tactic.\u00a0 The definition of is_RInt_gen<\/tt> then imposes that we show first that this function coincides with integrals at arbitrary bounds and second that this function has the right limit.\u00a0 The first part is expressed using a filterprod<\/tt> 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<\/tt> 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<\/tt> to deal with proving the derivability of functions. So we rely on the following theorem:<\/p>\n
ex_derive_continuous\r\n : forall (f : ?K -> ?V) (x : ?K), ex_derive f x -> continuous f x<\/pre>\n
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.\u00a0 In practice, I have the goal:<\/p>\n
============================\r\nforall x : R,\r\nRmin u v <= x <= Rmax u v ->\r\ncontinuous (fun x0 : R => \/ m * \/ (x0 \/ m * (x0 \/ m * 1) + 1)) x<\/pre>\n
and I need to type the following tactic.<\/p>\n
intros x _; apply (@ex_derive_continuous R_AbsRing R_NormedModule).\r\n<\/pre>\n
I guessed the arguments R_AbsRing<\/tt> and R_NormedModule<\/tt>, because the Check<\/tt> command on ex_derive_continuous<\/tt> indicated that the parameter K<\/tt> had to have type AbsRing<\/tt> and the parameter V had to have type NormedModule K<\/tt>.<\/p>\n
Once I have transformed the goal into proving that the integrand is derivable, the automatic tactic auto_derive<\/tt> finishes the job almost completely, again generating a side-condition to verify that the denominator is non-zero.<\/p>\n
Dealing with the limits<\/strong><\/p>\n
We need to prove that the limit of the function is \\(\\pi\\).\u00a0 This expressed with the following goal.<\/p>\n
============================\r\n   filterlim (fun p : R * R => atan (snd p \/ m) - atan (fst p \/ m))\r\n     (filter_prod (Rbar_locally m_infty) (Rbar_locally p_infty)) \r\n     (locally PI)<\/pre>\n
Here the predicate filterlim<\/tt> establishes a relation between an input filter (which describes the simultaneous limits
\nof two inputs towards minus infinity and plus infinity, respectively) and an output filter (which describes the limit towards \\(\\pi\\).<\/p>\n
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<\/tt> means that we need to consider
\nall 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<\/tt>) in my formal proof), so I can introduce all of them in the following manner.<\/p>\n
intros S HS; destruct HS as [ep Pep].\r\n<\/pre>\n
And the resulting goal has the following shape.<\/p>\n
\r\n  S : R_NormedModule -> Prop\r\n  ep : posreal\r\n  Pep : forall y : R_NormedModule, ball PI ep y -> S y\r\n  ============================\r\n   filtermap (fun p : R * R => atan (snd p \/ m) - atan (fst p \/ m))\r\n     (filter_prod (Rbar_locally m_infty) (Rbar_locally p_infty)) S<\/pre>\n
Here the predicate filtermap<\/tt> 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<\/tt>.  In this case, we will be
\nstronger and guarantee that the image is in the ball centered in \\(\\pi\\) with radius \\(\\varepsilon\\).<\/p>\n
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\\).<\/p>\n","protected":false},"excerpt":{"rendered":"
Today, I wish to show how to prove the computation of a well-known integral.\u00a0 I am using Coquelicot 2.1.1. The integral is as follows and m is positive. There is a lemma named is_RInt_derive with the following statement: forall (f df : R -> R) (a b : R), (forall\u2026<\/p>\n
 Continue reading<\/span><\/i><\/a> <\/p>\n","protected":false},"author":1013,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-91","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/posts\/91","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/users\/1013"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/comments?post=91"}],"version-history":[{"count":38,"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/posts\/91\/revisions"}],"predecessor-version":[{"id":243,"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/posts\/91\/revisions\/243"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/media?parent=91"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/categories?post=91"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/project.inria.fr\/coqexchange\/wp-json\/wp\/v2\/tags?post=91"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}