In mathematics, integrals of inverse functions can be computed by means of a formula that expresses the antiderivatives of the inverse
Statement of the theorem
In his 1905 article, Laisant gave three proofs. First, under the additional hypothesis that
The figure on the right is a proof without words of this formula. Laisant does not discuss the hypotheses necessary to make this proof rigorous, but it can be made explicit with the help of the Darboux integral (or Fubini's theorem if a demonstration based on the Lebesgue integral is desired). Laisant's third proof uses the additional hypothesis that
Nevertheless, it can be shown that this theorem holds even if
It is also possible to check that for every
To this end, it suffices to apply the mean value theorem to
- Assume that
f ( x ) = exp ( x ), hence f − 1 ( y ) = ln ( y ). The formula above gives immediately
∫ ln ( y ) d y = y ln ( y ) − y + C .
- Similarly, with
f ( x ) = cos ( x )and f − 1 ( y ) = arccos ( y ),
∫ arccos ( y ) d y = y arccos ( y ) − sin ( arccos ( y ) ) + C .
f ( x ) = tan ( x )and f − 1 ( y ) = arctan ( y ),
∫ arctan ( y ) d y = y arctan ( y ) + ln | cos ( arctan ( y ) ) | + C .
Apparently, this theorem of integration was discovered for the first time in 1905 by Charles-Ange Laisant, who "could hardly believe that this theorem is new", and hoped its use would henceforth spread out among students and teachers. This result was published independently in 1912 by an Italian engineer, Alberto Caprilli, in an opuscule entitled "Nuove formole d'integrazione". It was rediscovered in 1955 by Parker, and by a number of mathematicians following him. Nevertheless, they all assume that f or f−1 is differentiable. The general version of the theorem, free from this additional assumption, was proposed by Michael Spivak in 1965, as an exercise in the Calculus, and a fairly complete proof following the same lines was published by Eric Key in 1994. This proof relies on the very definition of the Darboux integral, and consists in showing that the upper Darboux sums of the function f are in 1-1 correspondence with the lower Darboux sums of f−1. In 2013, Michael Bensimhoun, estimating that the general theorem was still insufficiently known, gave two other proofs: The second proof, based on the Stieltjes integral and on its formulae of integration by parts and of homeomorphic change of variables, is the most suitable to establish more complex formulae.
Generalization to holomorphic functions
The above theorem generalizes in the obvious way to holomorphic functions: Let
Because all holomorphic functions are differentiable, the proof is immediate by complex differentiation.