∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [BorelSpace E] (r : E) (L : StrongDual ℝ E),
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun x => r + x) μ) L =
    MeasureTheory.charFunDual μ L * Complex.exp (↑(L r) * Complex.I)