Documentation

Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Binomial random graphs #

This file constructs the binomial distribution with parameter p on simple graphs with vertices V. This is the law G(V, p) of binomial random graphs with probability p.

TODO #

Add the characteristic predicate for a random graph to follow the binomial random distribution.

Historical note #

This is usually called the Erdős–Rényi model, but this name is historically inaccurate as Erdős and Rényi introduced a closely related but different model. We therefore choose the name "binomial random graph" to avoid confusion with this other model and because it is a more descriptive name.

Tags #

Erdős-Rényi graph, Erdős-Renyi graph, Erdös-Rényi graph, Erdös-Renyi graph, Erdos-Rényi graph, Erdos-Renyi graph

source
noncomputable def SimpleGraph.binomialRandom (V : Type u_1) (p : ↑unitInterval) :
MeasureTheory.Measure (SimpleGraph V)

The binomial distribution with parameter p on simple graphs with vertices V.

Equations
Instances For
    source
    def SimpleGraph.«termG(_,_)» :
    Lean.ParserDescr

    The binomial distribution with parameter p on simple graphs with vertices V.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem SimpleGraph.binomialRandom_eq_map (V : Type u_1) (p : ↑unitInterval) [Countable V] :
      binomialRandom V p = MeasureTheory.Measure.map fromEdgeSet (ProbabilityTheory.setBernoulli Sym2.diagSetᶜ p)
      source
      theorem SimpleGraph.binomialRandom_apply' {V : Type u_1} (p : ↑unitInterval) [Countable V] (S : Set (SimpleGraph V)) :
      (binomialRandom V p) S = (ProbabilityTheory.setBernoulli Sym2.diagSetᶜ p) (edgeSet '' S)
      source
      theorem SimpleGraph.binomialRandom_apply {V : Type u_1} (p : ↑unitInterval) [Countable V] (S : Set (SimpleGraph V)) :
      (binomialRandom V p) S = (MeasureTheory.Measure.infinitePi fun (e : Sym2 V) => (unitInterval.toNNReal p • MeasureTheory.Measure.dirac ¬e.IsDiag) + unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False) ((fun (G : SimpleGraph V) (e : Sym2 V) => e ∈ G.edgeSet) '' S)
      source
      instance SimpleGraph.instIsProbabilityMeasureBinomialRandom {V : Type u_1} {p : ↑unitInterval} [Countable V] :
      MeasureTheory.IsProbabilityMeasure (binomialRandom V p)
      source
      @[simp]
      theorem SimpleGraph.binomialRandom_zero (V : Type u_1) [Countable V] :
      binomialRandom V 0 = MeasureTheory.Measure.dirac ⊥
      source
      @[simp]
      theorem SimpleGraph.binomialRandom_one (V : Type u_1) [Countable V] :
      binomialRandom V 1 = MeasureTheory.Measure.dirac ⊤
      source
      @[simp]
      theorem SimpleGraph.binomialRandom_singleton {V : Type u_1} (p : ↑unitInterval) [Finite V] (G : SimpleGraph V) :
      (binomialRandom V p) {G} = ↑(unitInterval.toNNReal p) ^ G.edgeSet.ncard * ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)