# 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.

source
theorem Real.measurable_exp :
Measurable exp
source
theorem Real.measurable_log :
Measurable log
source
theorem Real.measurable_of_measurable_exp {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} (hf : Measurable fun (x : α) => exp (f x)) :
Measurable f
source
theorem Real.aemeasurable_of_aemeasurable_exp {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : AEMeasurable (fun (x : α) => exp (f x)) μ) :
AEMeasurable f μ
source
theorem Real.aemeasurable_of_aemeasurable_exp_mul {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α} {t : ℝ} (ht : t ≠ 0) (hf : AEMeasurable (fun (x : α) => exp (t * f x)) μ) :
AEMeasurable f μ
source
theorem Real.measurable_sin :
Measurable sin
source
theorem Real.measurable_cos :
Measurable cos
source
theorem Real.measurable_sinh :
Measurable sinh
source
theorem Real.measurable_cosh :
Measurable cosh
source
theorem Real.measurable_arcsin :
Measurable arcsin
source
theorem Real.measurable_arccos :
Measurable arccos
source
theorem Complex.measurable_re :
Measurable re
source
theorem Complex.measurable_im :
Measurable im
source
theorem Complex.measurable_ofReal :
Measurable ofReal
source
theorem Complex.measurable_exp :
Measurable exp
source
theorem Complex.measurable_sin :
Measurable sin
source
theorem Complex.measurable_cos :
Measurable cos
source
theorem Complex.measurable_sinh :
Measurable sinh
source
theorem Complex.measurable_cosh :
Measurable cosh
source
theorem Complex.measurable_arg :
Measurable arg
source
theorem Complex.measurable_log :
Measurable log
source
theorem Measurable.exp {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => Real.exp (f x)
source
theorem Measurable.log {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => Real.log (f x)
source
theorem Measurable.cos {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => Real.cos (f x)
source
theorem Measurable.sin {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => Real.sin (f x)
source
theorem Measurable.cosh {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => Real.cosh (f x)
source
theorem Measurable.sinh {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => Real.sinh (f x)
source
theorem Measurable.sqrt {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => √(f x)
source
theorem AEMeasurable.exp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Real.exp (f x)) μ
source
theorem AEMeasurable.log {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Real.log (f x)) μ
source
theorem AEMeasurable.cos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Real.cos (f x)) μ
source
theorem AEMeasurable.sin {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Real.sin (f x)) μ
source
theorem AEMeasurable.cosh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Real.cosh (f x)) μ
source
theorem AEMeasurable.sinh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Real.sinh (f x)) μ
source
theorem AEMeasurable.sqrt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => √(f x)) μ
source
theorem Measurable.cexp {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => Complex.exp (f x)
source
theorem Measurable.ccos {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => Complex.cos (f x)
source
theorem Measurable.csin {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => Complex.sin (f x)
source
theorem Measurable.ccosh {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => Complex.cosh (f x)
source
theorem Measurable.csinh {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => Complex.sinh (f x)
source
theorem Measurable.carg {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => (f x).arg
source
theorem Measurable.clog {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) :
Measurable fun (x : α) => Complex.log (f x)
source
theorem AEMeasurable.cexp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Complex.exp (f x)) μ
source
theorem AEMeasurable.ccos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Complex.cos (f x)) μ
source
theorem AEMeasurable.csin {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Complex.sin (f x)) μ
source
theorem AEMeasurable.ccosh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Complex.cosh (f x)) μ
source
theorem AEMeasurable.csinh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Complex.sinh (f x)) μ
source
theorem AEMeasurable.carg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => (f x).arg) μ
source
theorem AEMeasurable.clog {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => Complex.log (f x)) μ
source
theorem Measurable.complex_ofReal {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) :
Measurable fun (x : α) => ↑(f x)
source
theorem AEMeasurable.complex_ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => ↑(f x)) μ
source
instance Complex.hasMeasurablePow :
MeasurablePow ℂ ℂ
source
instance Real.hasMeasurablePow :
MeasurablePow ℝ ℝ
source
instance NNReal.hasMeasurablePow :
MeasurablePow NNReal ℝ
source
instance ENNReal.hasMeasurablePow :
MeasurablePow ENNReal ℝ