# mathlibdocumentation

measure_theory.function.special_functions

# 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, arctan, and scalar products.

theorem is_R_or_C.measurable_re {𝕜 : Type u_1} [is_R_or_C 𝕜] :
theorem is_R_or_C.measurable_im {𝕜 : Type u_1} [is_R_or_C 𝕜] :
theorem measurable.exp {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.exp (f x))
theorem measurable.log {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.log (f x))
theorem measurable.cos {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.cos (f x))
theorem measurable.sin {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sin (f x))
theorem measurable.cosh {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.cosh (f x))
theorem measurable.sinh {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sinh (f x))
theorem measurable.arctan {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.arctan (f x))
theorem measurable.sqrt {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sqrt (f x))
theorem measurable.cexp {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.exp (f x))
theorem measurable.ccos {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.cos (f x))
theorem measurable.csin {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.sin (f x))
theorem measurable.ccosh {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.cosh (f x))
theorem measurable.csinh {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.sinh (f x))
theorem measurable.carg {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), (f x).arg)
theorem measurable.clog {α : Type u_1} {m : measurable_space α} {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.log (f x))
theorem measurable.re {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {m : measurable_space α} {f : α → 𝕜} (hf : measurable f) :
measurable (λ (x : α), is_R_or_C.re (f x))
theorem ae_measurable.re {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {m : measurable_space α} {f : α → 𝕜} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), is_R_or_C.re (f x)) μ
theorem measurable.im {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {m : measurable_space α} {f : α → 𝕜} (hf : measurable f) :
measurable (λ (x : α), is_R_or_C.im (f x))
theorem ae_measurable.im {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {m : measurable_space α} {f : α → 𝕜} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), is_R_or_C.im (f x)) μ
theorem is_R_or_C.measurable_of_real {𝕜 : Type u_2} [is_R_or_C 𝕜] :
theorem measurable_of_re_im {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {f : α → 𝕜} (hre : measurable (λ (x : α), is_R_or_C.re (f x))) (him : measurable (λ (x : α), is_R_or_C.im (f x))) :
theorem ae_measurable_of_re_im {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {f : α → 𝕜} {μ : measure_theory.measure α} (hre : ae_measurable (λ (x : α), is_R_or_C.re (f x)) μ) (him : ae_measurable (λ (x : α), is_R_or_C.im (f x)) μ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [is_R_or_C 𝕜] [ E] {m : measurable_space α} {f g : α → E} (hf : measurable f) (hg : measurable g) :
measurable (λ (t : α), has_inner.inner (f t) (g t))
theorem ae_measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [is_R_or_C 𝕜] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → E} (hf : μ) (hg : μ) :
ae_measurable (λ (x : α), has_inner.inner (f x) (g x)) μ