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