mathlib3 documentation

measure_theory.function.special_functions.basic

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]
@[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))
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations