Elementary functions

Stream: mathlib4

[Trebor Huang]

I don't think there are elementary functions in mathlib (as a class of functions) yet? Since every individual type (sin, exp etc.) of functions is already in mathlib, I'd like to define the set of elementary functions and prove some elementary (no pun intended) properties. What is the best way to do this? One problem I can think of is that we also need to formalize the notion of "natural domain" of a function, which excludes zero for reciprocals, negative numbers for square roots, etc.

[Alex J. Best]

Generally we would define a class of functions like this using an inductive predicate, to express some fixed type of combinations of some fixed base functions. See docs#IsPoly or docs#IsSolvableByRad for some examples

[Trebor Huang]

Alex J. Best said:

Generally we would define a class of functions like this using an inductive predicate, to express some fixed type of combinations of some fixed base functions. See docs#IsPoly or docs#IsSolvableByRad for some examples

I'm thinking about either this or defining an inductive syntax (i.e. no indices, just an inductive type Elementary : Type), and a function Elementary -> Real -> Real that is zero outside of the natural domain.

[Trebor Huang]

I'm still worried about this domain thing. What should the value of $\frac{1}{x} + 1$ be at zero?

[Trebor Huang]

Also, we should have a theorem like "the floor function isn't elementary because it is not continuous on its domain". But if we use junk values I think this is false..

[Ruben Van de Velde]

Are you saying the floor function would be elementary, that it would be continuous, or that the implication "not continuous -> not elementary" would be false?

[Timo Carlin-Burns]

Could you define it as an inductive predicate on partial functions? docs#Nat.Partrec for an example

[Trebor Huang]

A quick sketch of my proposal before I go to bed:

Full Code

import Mathlib

inductive Syntax (V : Type) : Type where
| var : V → Syntax V
| const : ℝ → Syntax V
| root : Syntax V → ℕ → Syntax V
| add : Syntax V → Syntax V → Syntax V
| mul : Syntax V → Syntax V → Syntax V
| sin : Syntax V → Syntax V
| arcsin : Syntax V → Syntax V
| exp : Syntax V → Syntax V
| log : Syntax V → Syntax V

namespace Syntax

instance : Coe ℝ (Syntax V) where
  coe := .const

instance : Add (Syntax V) where
  add := .add

instance : Mul (Syntax V) where
  mul := .mul

instance : Neg (Syntax V) where
  neg f := (-1 : ℝ) * f

noncomputable def eval : Syntax V → (V → ℝ) → ℝ
| .var x, xs => xs x
| .const r, _ => r
| .root f n, xs => (eval f xs)^(1/(n+1))
| .add f g, xs => eval f xs + eval g xs
| .mul f g, xs => eval f xs * eval g xs
| .sin f, xs => Real.sin (eval f xs)
| .arcsin f, xs => Real.arcsin (eval f xs)
| .exp f, xs => Real.exp (eval f xs)
| .log f, xs => Real.log (eval f xs)

inductive InDomain : Syntax V → (V → ℝ) → Prop where
| var : InDomain (.var x) xs
| const : InDomain (.const r) xs
| root : InDomain f xs
  → f.eval xs >= 0
  → InDomain (.root f n) xs
| add : InDomain f xs → InDomain g xs → InDomain (f + g) xs
| mul : InDomain f xs → InDomain g xs → InDomain (f * g) xs
| sin : InDomain f xs → InDomain (.sin f) xs
| arcsin : InDomain f xs
  → f.eval xs ∈ Set.Icc (-1) 1
  → InDomain (.arcsin f) xs
| exp : InDomain f xs → InDomain (.exp f) xs
| log : InDomain f xs
  → f.eval xs > 0
  → InDomain (.log f) xs

[Trebor Huang]

Ruben Van de Velde said:

Are you saying the floor function would be elementary, that it would be continuous, or that the implication "not continuous -> not elementary" would be false?

The last. I think this is one of the "headline properties" of elementary functions, so we need to deal with it.

[Trebor Huang]

The rational roots look like a mess.. Let me see if there's some slick mathematical definition that avoids discussing the domain of ration powers