Measurability of complex powers with a real base

This file is a temporary home for a measurability result intended for the Mathlib theory of complex powers. It is independent of the multivariate Beta function.

theorem Complex.measurable_ofReal_cpow_const (c : ℂ) : Measurable fun (x : ℝ) => ↑x ^ c

Raising a real number, regarded as a complex number, to a fixed complex power is measurable. The possible discontinuity at zero does not affect measurability.