2
$\begingroup$

Two recent questions have asserted in comments that one may define $\exp x$ as the unique function on $\mathbb{R}$ for which we have $\exp'=\exp$ and $\exp 0=1$. Can one see directly that such a function exists? Or must one either (a) define the usual power series, prove it is convergent and differentiable everywhere, and so is a candidate for $\exp x$; or alternatively (b) define $\log x:=\int_{1}^{x}\frac{dt}{t}$ on $\mathbb{R}^{>0}$, prove enough about it to show that it has an inverse, which by the FTC is a candidate for $\exp$.

This related question Exponential Function - Definition seems to me to consist of mere assertions, but it does point one to Wikipedia: Characterizations of the Exponential Function, where the above "definition" is Characterization 4.

$\endgroup$
8
  • 4
    $\begingroup$ That really depends on what you can use. If you know some basic theory about differential equations then you can “see directly” that a unique solution to the initial value problem $y' = y$, $y(0) = 1$ exists. $\endgroup$
    – Martin R
    Commented Feb 15, 2021 at 15:50
  • $\begingroup$ In the normal course of mathematical learning, and if you want to be rigorous, I would expect that the existence of a unique solution to the differential equation would come later than the desirability of having the exponential function available, so to me better to define $\exp x$ by some other route than as the unique solution to $y'=y, y(0) = 0$. $\endgroup$
    – WA Don
    Commented Feb 15, 2021 at 15:56
  • $\begingroup$ @WADon: In my book a mature math learner would have a couple of different definitions of $\exp$ available, and have seen proofs of their equivalence. So, should that be the first definition they see? Probably not. Should they know it? Yes. $\endgroup$
    – JonathanZ
    Commented Feb 15, 2021 at 16:01
  • $\begingroup$ @MartinR I think I am asking for an account of this "basic theory about DE": is there some big theorem I seem to have missed which asserts the existence of a solution of certain sorts of DE? $\endgroup$ Commented Feb 15, 2021 at 16:02
  • 3
    $\begingroup$ @ancientmathematician The Picard–Lindelöf theorem is probably what you are looking for. $\endgroup$ Commented Feb 15, 2021 at 16:04

0

You must log in to answer this question.

Browse other questions tagged .