noncomputable def ProbabilityTheory.charFun (μ : MeasureTheory.Measure ℝ) (t : ℝ) : ℂ

The characteristic function of a probability measure μ on ℝ, defined by φ(t) = ∫ exp(i t x) dμ(x). For a random variable X with law μ this is φ_X(t) = E[exp(i t X)].

theorem ProbabilityTheory.charFun_eq_measureTheory_charFun (μ : MeasureTheory.Measure ℝ) (t : ℝ) : charFun μ t = MeasureTheory.charFun μ t

The local charFun defined here agrees with Mathlib's MeasureTheory.charFun on real measures, up to rearranging the order of multiplication inside the exponential.