Documentation

TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Defs

Exchangeable graph laws #

An exchangeable random graph on an unbounded label set is presented here by its finite marginals: a probability law on SimpleGraph (Fin k) for every k, consistent under pulling a graph back along every injection of labels Fin k ↪ Fin l. Consistency along all injections is a single hypothesis doing two jobs: the permutations of Fin k give invariance under relabelling, and the inclusions Fin k ↪ Fin (k + 1) give the projectivity that makes the family the finite-dimensional distributions of one random graph.

The observable through which a graph parameter reads off such a law is the upper mass of a finite pattern F: the probability P(F ≤ ·) that the level-k sample contains F. Upper masses take values in [0, 1], take the value 1 at the edgeless pattern, and are unchanged by relabelling a pattern along an injection — the consistency hypothesis seen on upper events. They are a complete observable: an upper mass is the total probability of the graphs above the pattern, so downward induction along the finite lattice of graphs recovers the probability of an individual graph, and hence the whole law, from the upper masses (MeasureTheory.Measure.ext_of_Ici_of_finite).

The label set is always a finite Fin k, so its graphs form a finite measurable space and every set of them is measurable; no measurability side conditions appear below.

Main definitions #

Main results #

References #

source
structure TauCeti.DenseGraphLimits.ExchangeableGraphLaw :
Type

An exchangeable random graph presented by its consistent finite marginals: a probability law on the graphs with labels Fin k for every k, consistent under pulling back along every injection of labels.

Instances For
    source
    instance TauCeti.DenseGraphLimits.ExchangeableGraphLaw.instIsProbabilityMeasureLaw (L : ExchangeableGraphLaw) (k : ℕ) :
    MeasureTheory.IsProbabilityMeasure (L.law k)
    source
    theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.ext {L L' : ExchangeableGraphLaw} (h : ∀ (k : ℕ), L.law k = L'.law k) :
    L = L'

    A law is determined by its marginals: the two remaining fields are propositions.

    source
    theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.ext_iff {L L' : ExchangeableGraphLaw} :
    L = L' ↔ ∀ (k : ℕ), L.law k = L'.law k
    source
    def TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) :
    ℝ

    The upper mass of a pattern F: the probability that the level-k sample contains F.

    Equations
    Instances For
      source
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_def (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) :
      L.upperMass F = ((L.law k) {G : SimpleGraph (Fin k) | F ≤ G}).toReal

      The defining probability of an upper mass.

      source
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_nonneg (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) :
      0 ≤ L.upperMass F

      An upper mass is nonnegative.

      source
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_le_one (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) :
      L.upperMass F ≤ 1

      An upper mass is at most 1.

      source
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_antitone (L : ExchangeableGraphLaw) {k : ℕ} :
      Antitone L.upperMass

      Strengthening a pattern shrinks its upper event, so upper masses are antitone.

      source
      @[simp]
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_bot (L : ExchangeableGraphLaw) {k : ℕ} :
      L.upperMass ⊥ = 1

      Every graph contains the edgeless pattern, so its upper mass is 1.

      source
      @[simp]
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_map (L : ExchangeableGraphLaw) {k l : ℕ} (F : SimpleGraph (Fin k)) (f : Fin k ↪ Fin l) :
      L.upperMass (SimpleGraph.map (⇑f) F) = L.upperMass F

      Upper masses are unchanged by relabelling the pattern along an injection: the event that the level-l sample contains the relabelled pattern is the event that its restriction to the window contains the original one.

      source
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_eq_sum (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) :
      L.upperMass F = ∑ G : SimpleGraph (Fin k) with F ≤ G, ((L.law k) {G}).toReal

      An upper mass is the total probability of the individual graphs containing the pattern: the label set is finite, so the upper event is a finite union of singletons.

      source
      theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.ext_upperMass {L L' : ExchangeableGraphLaw} (h : ∀ (k : ℕ) (F : SimpleGraph (Fin k)), L.upperMass F = L'.upperMass F) :
      L = L'

      The upper masses determine the law. An upper mass is the mass of an upper ray in the finite lattice of graphs, and a finite measure on a finite partial order is determined by its upper rays: downward induction along the lattice recovers the probability of every individual graph.