Euler's number e

Stream: Is there code for X?

[Iocta]

I see there is the Real.exp function. Is the number e defined?

[Riccardo Brasca]

It is Real.exp 1. I don't think there is a notation for it

[Riccardo Brasca]

In the sense that when we need it we just write Real.exp 1.

[Jireh Loreaux]

There is a unicode character for this: U+2107 ℇ, but that looks an awful lot like epsilon. Potentially we could use 𝑒, which is U+1D452, in the Real scope.

[Edward van de Meent]

i think introducing that notation might trick people into writing e^x rather than Real.exp x, which might lead to defeq problems?

[Kyle Miller]

It's probably not a good idea, but that could be addressed with a macro:

notation "𝑒" => Real.exp 1

macro_rules | `(𝑒 ^ $x) => `(Real.exp $x)

#check 𝑒 ^ 2
-- Real.exp 2

[Vincent Beffara]

But then other people would write e^z to mean Complex.exp z

[Edward van de Meent]

then something like

import Mathlib.Data.Complex.Basic

class NaturalExp (R:Type*) where
  exp : R -> R -- possibly more fields, i'm not sure what kind of requirements are natural here

noncomputable instance : NaturalExp Real where
  exp := Real.exp

noncomputable instance : NaturalExp Complex where
  exp := Complex.exp

notation "𝑒" => NaturalExp.exp 1

macro_rules | `(𝑒 ^ $x) => `(NaturalExp.exp $x)

example : 𝑒 ^ 2 = Real.exp 2 := rfl

example : 𝑒 ^ 2 = Complex.exp 2 := rfl

[Edward van de Meent]

i imagine fields like exp_add and exp_zero are some natural conditions... but these aren't sufficient conditions to uniquely define (𝑒 ^ .)

[Eric Rodriguez]

If it's just a notation class we usually don't need to add conditions

[Edward van de Meent]

i suppose that's fair...

[Edward van de Meent]

but i imagine unifying the api involved would be useful...

[Edward van de Meent]

and i think that takes more than just a notation class

[Eric Rodriguez]

I don't know if it's wise to unify the API, just let lemmas for all the different exps apply IMO

[Eric Wieser]

Don't forget docs#NormedSpace.exp

[Jireh Loreaux]

I think we don't need the macro expansion for 𝑒 ^ x if we just put in the docstring for the notation that it should only be used for Real.exp 1.

[Eric Wieser]

elab_rules | `(𝑒 ^ $x) => throwError "don't do this"

[Mario Carneiro]

that could be a linter...

[Edward van de Meent]

linters like this can be elab_rules, you mean? :upside_down:

[Eric Wieser]

Mario Carneiro said:

that could be a linter...

What's the difference between a linter and an elaborator that throws a warning using logLint?

[Damiano Testa]

It is easier to silence the linter than the elaborator.

[Eric Wieser]

Well, if the elaborator calls docs#Lean.Linter.logLintIf then the silencing mechanism is unchanged

[Mario Carneiro]

Note, I count "fake linters" that run during elaboration but use logLint as linters for this purpose

[Mario Carneiro]

(an example of which is linter.deprecated)