# Documentation

Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

# Measurability of real and complex functions #

We show that most standard real and complex functions are measurable, notably exp, cos, sin, cosh, sinh, log, pow, arcsin, arccos.

See also MeasureTheory.Function.SpecialFunctions.Arctan and MeasureTheory.Function.SpecialFunctions.Inner, which have been split off to minimize imports.

theorem Measurable.exp {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.exp (f x)
theorem Measurable.log {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.log (f x)
theorem Measurable.cos {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.cos (f x)
theorem Measurable.sin {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.sin (f x)
theorem Measurable.cosh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.cosh (f x)
theorem Measurable.sinh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.sinh (f x)
theorem Measurable.sqrt {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Real.sqrt (f x)
theorem Measurable.cexp {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.exp (f x)
theorem Measurable.ccos {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.cos (f x)
theorem Measurable.csin {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.sin (f x)
theorem Measurable.ccosh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.cosh (f x)
theorem Measurable.csinh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.sinh (f x)
theorem Measurable.carg {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.arg (f x)
theorem Measurable.clog {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun x => Complex.log (f x)