# 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 Real.measurable_of_measurable_exp {α : Type u_1} :
∀ {x : } {f : α}, (Measurable fun (x : α) => Real.exp (f x))
theorem Real.aemeasurable_of_aemeasurable_exp {α : Type u_1} :
∀ {x : } {f : α} {μ : }, (AEMeasurable fun (x : α) => Real.exp (f x))
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)
Equations
Equations
Equations
Equations