Measurability of real and complex functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
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))
@[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}