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]
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
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)) μ) :
ae_measurable f μ
@[protected, instance]
Equations
- complex.has_measurable_pow = {measurable_pow := complex.has_measurable_pow._proof_1}
@[protected, instance]
Equations
- real.has_measurable_pow = {measurable_pow := real.has_measurable_pow._proof_1}
@[protected, instance]
Equations
- nnreal.has_measurable_pow = {measurable_pow := nnreal.has_measurable_pow._proof_1}
@[protected, instance]
Equations
- ennreal.has_measurable_pow = {measurable_pow := ennreal.has_measurable_pow._proof_1}