# 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 : α) => (f x).exp)
theorem Real.aemeasurable_of_aemeasurable_exp {α : Type u_1} :
∀ {x : } {f : α} {μ : }, AEMeasurable (fun (x : α) => (f x).exp) μ
theorem Measurable.exp {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).exp
theorem Measurable.log {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).log
theorem Measurable.cos {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).cos
theorem Measurable.sin {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).sin
theorem Measurable.cosh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).cosh
theorem Measurable.sinh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).sinh
theorem Measurable.sqrt {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x)
theorem Measurable.cexp {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).exp
theorem Measurable.ccos {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).cos
theorem Measurable.csin {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).sin
theorem Measurable.ccosh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).cosh
theorem Measurable.csinh {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).sinh
theorem Measurable.carg {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).arg
theorem Measurable.clog {α : Type u_1} {m : } {f : α} (hf : ) :
Measurable fun (x : α) => (f x).log
Equations
Equations
Equations
Equations