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