a characterization of real.exp

Stream: maths

[David Renshaw]

Hi, while working on an olympiad problem, I ended up needing to prove the following lemma:

lemma exp_characterization
    (u : ℝ → ℝ)
    (hu : ∀ x y : ℝ, u (x + y) = u x * u y)
    (hu0 : u 0 = 1)
    (hm : strict_mono u ∨ strict_anti u) :
    (∃ k : ℝ, ∀ x : ℝ, u x = real.exp (k * x)) := ...

(see my proof, which is long and tedious, here)

This feels like the kind of thing where there might already exist some relevant lemmas in mathlib.
Does anyone know of any? (Or does anyone want to help me golf the proof?)

[Joseph Myers]

This feels like it should be done via reduction to Cauchy's functional equation (so try to get #12933 into mathlib).

[Yaël Dillies]

What Joseph said!