theorem
Measurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
(hf : Measurable f)
:
Measurable fun (x : α) => RCLike.re (f x)
theorem
AEMeasurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => RCLike.re (f x)) μ
theorem
Measurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
(hf : Measurable f)
:
Measurable fun (x : α) => RCLike.im (f x)
theorem
AEMeasurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => RCLike.im (f x)) μ
theorem
measurable_of_re_im
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
[MeasurableSpace α]
{f : α → 𝕜}
(hre : Measurable fun (x : α) => RCLike.re (f x))
(him : Measurable fun (x : α) => RCLike.im (f x))
:
theorem
aemeasurable_of_re_im
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
[MeasurableSpace α]
{f : α → 𝕜}
{μ : MeasureTheory.Measure α}
(hre : AEMeasurable (fun (x : α) => RCLike.re (f x)) μ)
(him : AEMeasurable (fun (x : α) => RCLike.im (f x)) μ)
:
AEMeasurable f μ