Facts about Gaussian characteristic function

theorem ProbabilityTheory.HasGaussianLaw.map_eq_gaussianReal {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : HasGaussianLaw X P) : MeasureTheory.Measure.map X P = gaussianReal (∫ (x : Ω), X x ∂P) (variance X P).toNNReal

theorem ProbabilityTheory.HasGaussianLaw.charFun_map_real {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : HasGaussianLaw X P) (t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map X P) t = Complex.exp ((↑t * ∫ (x : Ω), ↑(X x) ∂P) * Complex.I - ↑t ^ 2 * ↑(variance X P) / 2)