Integral of complex functions

Stream: Is there code for X?

[Jason KY.]

Do we have something like this?

lemma integrable.integral_eq_coe_re_add_coe_im {f : α → ℂ} (hf : integrable f μ) :
  ∫ x, f x ∂μ = ∫ x, (f x).re ∂μ + ∫ x, (f x).im ∂μ * complex.I :=

If not which file should it belong in?

[Jason KY.]

I created #9735 for this lemma (generalized to is_R_or_C). Do tell me if it is there already/I placed the lemmas in the wrong file.

[Yury G. Kudryashov]

I think that we should add instances [is_R_or_C k] : measurable_space k and [is_R_or_C k] : borel_space k.

[Yury G. Kudryashov]

Both instances have measurable_space defeq to borel anyway.

[Yury G. Kudryashov]

(but this might be out of the scope for this PR)