Theorems · Theorem · measure theory

MeasureTheory.charFunDual_map_add_const

∀ {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 => x + r) μ) L =
    MeasureTheory.charFunDual μ L * Complex.exp (↑(L r) * Complex.I)

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

1 results in Mathlib

Foundations

Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceBorelSpace