Theorems · Theorem · probability

SimpleGraph.binomialRandom_apply

∀ {V : Type u_1} (p : ↑unitInterval) [Countable V] (S : Set (SimpleGraph V)),
  (SimpleGraph.binomialRandom V p) S =
    (MeasureTheory.Measure.infinitePi fun e =>
        (unitInterval.toNNReal p • MeasureTheory.Measure.dirac ¬e.IsDiag) +
          unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)
      ((fun G e => e ∈ G.edgeSet) '' S)

Defined in

Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

Countable