Theorems · Theorem · probability

ProbabilityTheory.setBernoulli_eq_map

∀ {ι : Type u_1} (u : Set ι) (p : ↑unitInterval),
  ProbabilityTheory.setBernoulli u p =
    MeasureTheory.Measure.map (fun p => {i | p i})
      (MeasureTheory.Measure.infinitePi fun i =>
        unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) +
          unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)

Defined in

Mathlib.Probability.Distributions.SetBernoulli

Cited by

2 results in Mathlib

Foundations

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