mathlib documentation

measure_theory.function.special_functions.basic

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 measure_theory.function.special_functions.arctan and measure_theory.function.special_functions.inner, which have been split off to minimize imports.

@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
@[measurability]
theorem measurable.exp {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), rexp (f x))
@[measurability]
theorem measurable.log {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), real.log (f x))
@[measurability]
theorem measurable.cos {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), real.cos (f x))
@[measurability]
theorem measurable.sin {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), real.sin (f x))
@[measurability]
theorem measurable.cosh {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), real.cosh (f x))
@[measurability]
theorem measurable.sinh {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), real.sinh (f x))
@[measurability]
theorem measurable.sqrt {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem measurable.cexp {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), cexp (f x))
@[measurability]
theorem measurable.ccos {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), complex.cos (f x))
@[measurability]
theorem measurable.csin {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), complex.sin (f x))
@[measurability]
theorem measurable.ccosh {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), complex.cosh (f x))
@[measurability]
theorem measurable.csinh {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), complex.sinh (f x))
@[measurability]
theorem measurable.carg {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), (f x).arg)
@[measurability]
theorem measurable.clog {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), complex.log (f x))
@[measurability]
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))
@[measurability]
theorem ae_measurable.re {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {m : measurable_space α} {f : α 𝕜} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), is_R_or_C.re (f x)) μ
@[measurability]
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))
@[measurability]
theorem ae_measurable.im {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {m : measurable_space α} {f : α 𝕜} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), is_R_or_C.im (f x)) μ
@[measurability]
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 𝕜] [measurable_space α] {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 𝕜] [measurable_space α] {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