Theorems · Theorem · probability

ProbabilityTheory.hasLaw_dirac_iff

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] [MeasurableSingletonClass 𝓧] {x : 𝓧},
  ProbabilityTheory.HasLaw X (MeasureTheory.Measure.dirac x) P ↔ X =ᵐ[P] fun x_1 => x

Defined in

Mathlib.Probability.HasLaw

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureMeasurableSingletonClass