Documentation

TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Dissociated

Dissociated exchangeable graph laws #

An exchangeable graph law is dissociated when the random graph restricted to two disjoint windows of labels consists of two independent pieces: the level-(k + l) marginal, pushed to the pair of graphs it induces on the first k and on the last l labels, is the product of the level-k and level-l marginals. By exchangeability two disjoint windows of sizes k and l can be relabelled as the first k and the next l labels, and by consistency the labels beyond them can then be dropped, so the first k and the last l labels of Fin (k + l) suffice.

Dissociation is an identity between two laws on pairs of graphs, while the upper masses of a law only see its upper events. The two meet in the bridge isDissociated_iff_upperMass_mul: a law is dissociated exactly when its upper masses are multiplicative over disjoint unions of patterns. One direction reads the multiplicativity off the upper rectangles. The other needs that the upper rectangles determine a law on pairs of graphs, which is Möbius inversion over the product of the two finite lattices of graphs — the downward induction of MeasureTheory.Measure.ext_of_Ici_of_finite, since the upper ray at a pair of patterns is the rectangle of their upper events.

Main definitions #

Main results #

References #

source
def TauCeti.DenseGraphLimits.ExchangeableGraphLaw.IsDissociated (L : ExchangeableGraphLaw) :
Prop

A law is dissociated when restrictions to disjoint label windows are independent: the level-(k + l) marginal pushed to the pair of windows is the product of the level-k and level-l marginals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.isDissociated_iff (L : ExchangeableGraphLaw) :
    L.IsDissociated ↔ ∀ (k l : ℕ), MeasureTheory.Measure.map (fun (G : SimpleGraph (Fin (k + l))) => (SimpleGraph.comap (Fin.castAdd l) G, SimpleGraph.comap (Fin.natAdd k) G)) (L.law (k + l)) = (L.law k).prod (L.law l)

    The defining identity of a dissociated law: the level-(k + l) marginal pushed to the pair of windows is the product of the level-k and level-l marginals.

    source
    theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.upperMass_map_sum (L : ExchangeableGraphLaw) {k l : ℕ} (F₁ : SimpleGraph (Fin k)) (F₂ : SimpleGraph (Fin l)) :
    L.upperMass (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F₁ ⊕g F₂)) = ((MeasureTheory.Measure.map (fun (G : SimpleGraph (Fin (k + l))) => (SimpleGraph.comap (Fin.castAdd l) G, SimpleGraph.comap (Fin.natAdd k) G)) (L.law (k + l))) (Set.Ici F₁ ×ˢ Set.Ici F₂)).toReal

    The upper mass of a disjoint union of two patterns, placed on the first k and the last l labels, is the mass of the rectangle of their two upper events under the law of the pair of windows: a graph contains the union exactly when its two windows contain the two patterns.

    source
    theorem TauCeti.DenseGraphLimits.isDissociated_iff_upperMass_mul (L : ExchangeableGraphLaw) :
    L.IsDissociated ↔ ∀ (k l : ℕ) (F₁ : SimpleGraph (Fin k)) (F₂ : SimpleGraph (Fin l)), L.upperMass (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F₁ ⊕g F₂)) = L.upperMass F₁ * L.upperMass F₂

    Dissociation via upper masses. A law is dissociated iff its upper masses are multiplicative over disjoint unions of patterns. The forward direction evaluates the two laws on upper rectangles; the converse holds because the upper rectangles are the upper rays of the product of the two finite lattices of graphs, which determine a finite law on it.