theorem
ProbabilityTheory.hasLaw_map
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : AEMeasurable X P)
:
HasLaw X (MeasureTheory.Measure.map X P) P
theorem
ProbabilityTheory.HasLaw.ae_eq_of_dirac'
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSingletonClass 𝓧]
{x : 𝓧}
{X : Ω → 𝓧}
(hX : HasLaw X (MeasureTheory.Measure.dirac x) P)
:
theorem
ProbabilityTheory.HasLaw.ae_eq_of_dirac
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSingletonClass 𝓧]
{x : 𝓧}
{X : Ω → 𝓧}
(hX : HasLaw X (MeasureTheory.Measure.dirac x) P)
:
theorem
ProbabilityTheory.HasLaw.ae_eq_const_of_gaussianReal
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{μ : ℝ}
(hX : HasLaw X (gaussianReal μ 0) P)
: