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 Real.exp

theorem Real.measurable_log : Measurable Real.log

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

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

theorem Real.measurable_sin : Measurable Real.sin

theorem Real.measurable_cos : Measurable Real.cos

theorem Real.measurable_sinh : Measurable Real.sinh

theorem Real.measurable_cosh : Measurable Real.cosh

theorem Real.measurable_arcsin : Measurable Real.arcsin

theorem Real.measurable_arccos : Measurable Real.arccos

theorem Complex.measurable_re : Measurable Complex.re

theorem Complex.measurable_im : Measurable Complex.im

theorem Complex.measurable_ofReal : Measurable Complex.ofReal'

theorem Complex.measurable_exp : Measurable Complex.exp

theorem Complex.measurable_sin : Measurable Complex.sin

theorem Complex.measurable_cos : Measurable Complex.cos

theorem Complex.measurable_sinh : Measurable Complex.sinh

theorem Complex.measurable_cosh : Measurable Complex.cosh

theorem Complex.measurable_arg : Measurable Complex.arg

theorem Complex.measurable_log : Measurable Complex.log

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

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

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

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

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

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

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 : α) => (f x).exp

theorem Measurable.ccos {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) : Measurable fun (x : α) => (f x).cos

theorem Measurable.csin {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) : Measurable fun (x : α) => (f x).sin

theorem Measurable.ccosh {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) : Measurable fun (x : α) => (f x).cosh

theorem Measurable.csinh {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) : Measurable fun (x : α) => (f x).sinh

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 : α) => (f x).log

instance Complex.hasMeasurablePow : MeasurablePow ℂ ℂ

Equations

• Complex.hasMeasurablePow = ⋯

instance Real.hasMeasurablePow : MeasurablePow ℝ ℝ

Equations

• Real.hasMeasurablePow = ⋯

instance NNReal.hasMeasurablePow : MeasurablePow NNReal ℝ

Equations

• NNReal.hasMeasurablePow = ⋯

instance ENNReal.hasMeasurablePow : MeasurablePow ENNReal ℝ

Equations

• ENNReal.hasMeasurablePow = ⋯