Zulip Chat Archive

Stream: maths

Topic: a characterization of real.exp


David Renshaw (Dec 21 2022 at 01:33):

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 (Dec 21 2022 at 02:12):

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

Yaël Dillies (Dec 21 2022 at 07:36):

What Joseph said!


Last updated: Dec 20 2023 at 11:08 UTC