theorem ProbabilityTheory.HasLaw.ae_eq_const_of_gaussianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {μ : ℝ} (hX : HasLaw X (gaussianReal μ 0) P) : ∀ᵐ (ω : Ω) ∂P, X ω = μ