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_exp : Measurable exp

theorem Real.measurable_log : Measurable log

theorem Real.measurable_of_measurable_exp {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} (hf : Measurable fun (x : α) => exp (f x)) : Measurable f

theorem Real.aemeasurable_of_aemeasurable_exp {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : AEMeasurable (fun (x : α) => exp (f x)) μ) : AEMeasurable f μ

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 μ

theorem Real.measurable_sin : Measurable sin

theorem Real.measurable_cos : Measurable cos

theorem Real.measurable_sinh : Measurable sinh

theorem Real.measurable_cosh : Measurable cosh

theorem Real.measurable_arcsin : Measurable arcsin

theorem Real.measurable_arccos : Measurable arccos

theorem Complex.measurable_re : Measurable re

theorem Complex.measurable_im : Measurable im

theorem Complex.measurable_ofReal : Measurable ofReal

theorem Complex.measurable_exp : Measurable exp

theorem Complex.measurable_sin : Measurable sin

theorem Complex.measurable_cos : Measurable cos

theorem Complex.measurable_sinh : Measurable sinh

theorem Complex.measurable_cosh : Measurable cosh

theorem Complex.measurable_arg : Measurable arg

theorem Complex.measurable_log : Measurable log

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 AEMeasurable.exp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.exp (f x)) μ

theorem AEMeasurable.log {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.log (f x)) μ

theorem AEMeasurable.cos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.cos (f x)) μ

theorem AEMeasurable.sin {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.sin (f x)) μ

theorem AEMeasurable.cosh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.cosh (f x)) μ

theorem AEMeasurable.sinh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.sinh (f x)) μ

theorem AEMeasurable.sqrt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (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)

theorem AEMeasurable.cexp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Complex.exp (f x)) μ

theorem AEMeasurable.ccos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Complex.cos (f x)) μ

theorem AEMeasurable.csin {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Complex.sin (f x)) μ

theorem AEMeasurable.ccosh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Complex.cosh (f x)) μ

theorem AEMeasurable.csinh {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Complex.sinh (f x)) μ

theorem AEMeasurable.carg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => (f x).arg) μ

theorem AEMeasurable.clog {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Complex.log (f x)) μ

theorem Measurable.complex_ofReal {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) : Measurable fun (x : α) => ↑(f x)

theorem AEMeasurable.complex_ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => ↑(f x)) μ

instance Complex.hasMeasurablePow : MeasurablePow ℂ ℂ

instance Real.hasMeasurablePow : MeasurablePow ℝ ℝ

instance NNReal.hasMeasurablePow : MeasurablePow NNReal ℝ

instance ENNReal.hasMeasurablePow : MeasurablePow ENNReal ℝ