mathlib documentation

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 measurable.exp {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.exp (f x))
theorem measurable.log {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.log (f x))
theorem measurable.cos {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.cos (f x))
theorem measurable.sin {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sin (f x))
theorem measurable.cosh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.cosh (f x))
theorem measurable.sinh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sinh (f x))
theorem measurable.arctan {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.arctan (f x))
theorem measurable.sqrt {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), real.sqrt (f x))
theorem measurable.cexp {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.exp (f x))
theorem measurable.ccos {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.cos (f x))
theorem measurable.csin {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.sin (f x))
theorem measurable.ccosh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.cosh (f x))
theorem measurable.csinh {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), complex.sinh (f x))
theorem measurable.carg {α : Type u_1} [measurable_space α] {f : α → } (hf : measurable f) :
measurable (λ (x : α), (f x).arg)
theorem measurable.clog {α : Type u_1} [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 𝕜] [measurable_space α] [measurable_space 𝕜] [opens_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 𝕜] [measurable_space α] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), is_R_or_C.re (f x)) μ
theorem measurable.im {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [measurable_space α] [measurable_space 𝕜] [opens_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 𝕜] [measurable_space α] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), is_R_or_C.im (f x)) μ
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [measurable_space α] [measurable_space E] [opens_measurable_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] {f g : α → E} (hf : measurable f) (hg : measurable g) :
measurable (λ (t : α), inner (f t) (g t))
theorem ae_measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [measurable_space α] [measurable_space E] [opens_measurable_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] {μ : measure_theory.measure α} {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), inner (f x) (g x)) μ