Theorems · Inductive type · probability

ProbabilityTheory.HasLaw

{Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {m𝓧 : MeasurableSpace 𝓧} →
        (Ω → 𝓧) → MeasureTheory.Measure 𝓧 → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1 → Prop

The predicate HasLaw X μ P registers the fact that the random variable X has law μ under the measure P, in other words that P.map X = μ. We also require X to be AEMeasurable, to allow for nice interactions with operations on the codomain of X. See for instance HasLaw.comp, IndepFun.hasLaw_mul and IndepFun.hasLaw_add.

Defined in

Mathlib.Probability.HasLaw

Cited by

69 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms