Exchangeable directed-graph laws: the PMF-based finite API (directed umbrella #84, D2 / #86)

The directed specialization of the generic exchangeable-law theory (R2, issue #105). Because digraphSig has finitely many relation symbols, a finite directed law over Fin k is a genuine probability mass function PMF (Digraph (Fin k)) — the conventional combinatorial object — rather than a ProbabilityMeasure on the (uncountable) relational carrier. This file provides that user-facing PMF-based API and bridges it to the measure-side RelExchangeableLaw digraphSig, then composes with the R2c equivalence to obtain the headline finite/infinite directed equivalence.

• finiteDigraphEquiv_restrict / finiteDigraphEquiv_symm_restrict — the finite carrier equivalence commutes with restriction: Digraph.comap on the combinatorial side matches RelStructure.restrict on the relational side (via digraphStructureEquiv_comap);
• ExchangeableDigraphLaw — the PMF-based finite directed law: a PMF (Digraph (Fin k)) for each k, consistent under Digraph.comap along every Fin k ↪ Fin l;
• digraphLawEquiv — the finite bridge ExchangeableDigraphLaw ≃ RelExchangeableLaw digraphSig, transporting via finiteDigraphEquiv and the PMF.toMeasure / Measure.toPMF correspondence;
• InfiniteExchangeableDigraphLaw — the infinite directed law (a relabelling-invariant law on the infinite digraph space InfiniteDigraph, where the measurable structure lives);
• exchangeableDigraphLawEquiv — the headline directed equivalence ExchangeableDigraphLaw ≃ InfiniteExchangeableDigraphLaw, the composite of the finite bridge with the R2c relational equivalence.

The measurable / topological structure is used only on the relational carrier (InfiniteDigraph / FiniteDigraph); Mathlib's Digraph carries no measurable-space instance. The finite PMF ↔ ProbabilityMeasure conversions are localized to the bridge maps.

The finite carrier equivalence commutes with restriction

theorem digraphStructureEquiv_comap {V : Type u_1} {W : Type u_2} (f : V → W) (X : digraphSig.RelStructure fun (x : digraphSig.Srt) => W) : (digraphStructureEquiv V) (RelSignature.RelStructure.comap (fun (x : digraphSig.Srt) => f) X) = Digraph.comap f ((digraphStructureEquiv W) X)

The carrier equivalence commutes with comap: pulling a relational structure back along a constant sortwise map and then reading it as a digraph is the same as reading it as a digraph and pulling that back. The directed analogue of SimpleGraph.comap naturality.

theorem finiteDigraphEquiv_restrict {k l : ℕ} (e : Fin k ↪ Fin l) : (fun (G : Digraph (Fin l)) => Digraph.comap (⇑e) G) ∘ ⇑(finiteDigraphEquiv l) = ⇑(finiteDigraphEquiv k) ∘ RelSignature.RelStructure.restrict fun (x : Unit) => e

Restriction commutes with the finite carrier equivalence (forward form): reading a digraph off a relational structure and then Digraph.comap-ping is the same as RelStructure.restrict-ing and then reading it off.

theorem finiteDigraphEquiv_symm_restrict {n m : Unit → ℕ} (e : (s : Unit) → Fin (n s) ↪ Fin (m s)) : RelSignature.RelStructure.restrict e ∘ ⇑(finiteDigraphEquiv (m ())).symm = ⇑(finiteDigraphEquiv (n ())).symm ∘ fun (G : Digraph (Fin (m ()))) => Digraph.comap (⇑(e ())) G

Restriction commutes with the finite carrier equivalence (inverse form): the shape needed to transport PMF-marginals along finiteDigraphEquiv.symm.

The PMF-based finite directed law

structure ExchangeableDigraphLaw : Type

An exchangeable directed-graph law, presented by its consistent finite marginals: a PMF (Digraph (Fin k)) for every k, consistent under Digraph.comap along every injection of labels. The directed analogue of Graphon.ExchangeableGraphLaw; the marginals are PMFs because digraphSig is a finite signature.

• law (k : ℕ) : PMF (Digraph (Fin k))

  The k-vertex directed-graph marginal.

• consistent {k l : ℕ} (e : Fin k ↪ Fin l) : PMF.map (fun (G : Digraph (Fin l)) => Digraph.comap (⇑e) G) (self.law l) = self.law k

  Consistency under Digraph.comap along every injection of labels.

theorem ExchangeableDigraphLaw.ext {L M : ExchangeableDigraphLaw} (h : ∀ (k : ℕ), L.law k = M.law k) : L = M

theorem ExchangeableDigraphLaw.ext_iff {L M : ExchangeableDigraphLaw} : L = M ↔ ∀ (k : ℕ), L.law k = M.law k

noncomputable def ExchangeableDigraphLaw.toRel (D : ExchangeableDigraphLaw) : digraphSig.RelExchangeableLaw

The measure-side marginals of a PMF-based directed law: transport each PMF (Digraph (Fin k)) across finiteDigraphEquiv.symm and read it as a probability measure on the relational carrier.

Equations

• D.toRel = { marginal := fun (n : digraphSig.Srt → ℕ) => ⟨(PMF.map (⇑(finiteDigraphEquiv (n ())).symm) (D.law (n ()))).toMeasure, ⋯⟩, consistent := ⋯ }

@[simp]

theorem ExchangeableDigraphLaw.toRel_coe_marginal (D : ExchangeableDigraphLaw) (n : Unit → ℕ) : ↑(D.toRel.marginal n) = (PMF.map (⇑(finiteDigraphEquiv (n ())).symm) (D.law (n ()))).toMeasure

noncomputable def RelSignature.RelExchangeableLaw.toDigraph (L : digraphSig.RelExchangeableLaw) : ExchangeableDigraphLaw

The PMF-marginals of a measure-side directed law: read each relational marginal as a PMF (Measure.toPMF, the carrier is finite) and transport it across finiteDigraphEquiv.

Equations

• L.toDigraph = { law := fun (k : ℕ) => PMF.map (⇑(finiteDigraphEquiv k)) (↑(L.marginal fun (x : digraphSig.Srt) => k)).toPMF, consistent := ⋯ }

@[simp]

theorem RelSignature.RelExchangeableLaw.toDigraph_law (L : digraphSig.RelExchangeableLaw) (k : ℕ) : L.toDigraph.law k = PMF.map (⇑(finiteDigraphEquiv k)) (↑(L.marginal fun (x : digraphSig.Srt) => k)).toPMF

noncomputable def digraphLawEquiv : ExchangeableDigraphLaw ≃ digraphSig.RelExchangeableLaw

The finite directed bridge: PMF-based exchangeable directed-graph laws are the same data as measure-side exchangeable relational laws over digraphSig, with finiteDigraphEquiv and the PMF ↔ ProbabilityMeasure correspondence as inverse transports.

Equations

• digraphLawEquiv = { toFun := ExchangeableDigraphLaw.toRel, invFun := RelSignature.RelExchangeableLaw.toDigraph, left_inv := digraphLawEquiv._proof_1, right_inv := digraphLawEquiv._proof_2 }

@[simp]

theorem digraphLawEquiv_apply (D : ExchangeableDigraphLaw) : digraphLawEquiv D = D.toRel

@[simp]

theorem digraphLawEquiv_symm_apply (L : digraphSig.RelExchangeableLaw) : digraphLawEquiv.symm L = L.toDigraph

The infinite directed law and the headline equivalence

@[reducible, inline]

abbrev InfiniteExchangeableDigraphLaw : Type

An infinite exchangeable directed-graph law: a probability law on the infinite digraph space InfiniteDigraph invariant under every relabelling of ℕ. The measurable structure lives on the relational carrier, so this is the digraphSig specialization of InfiniteRelExchangeableLaw.

Equations

• InfiniteExchangeableDigraphLaw = digraphSig.InfiniteRelExchangeableLaw

noncomputable def exchangeableDigraphLawEquiv : ExchangeableDigraphLaw ≃ InfiniteExchangeableDigraphLaw

The directed finite/infinite exchangeable-law equivalence: PMF-based exchangeable directed-graph laws are the same data as relabelling-invariant laws on the infinite digraph space — the finite bridge digraphLawEquiv composed with the R2c relational equivalence relExchangeableLawEquiv. (This is the projective-law equivalence; the directed representation theorem — a mixture over digraphons — is later, D3/D4.)

Equations

• exchangeableDigraphLawEquiv = digraphLawEquiv.trans RelSignature.relExchangeableLawEquiv

@[simp]

theorem exchangeableDigraphLawEquiv_apply_law (D : ExchangeableDigraphLaw) : (exchangeableDigraphLawEquiv D).law = D.toRel.infiniteLaw

theorem exchangeableDigraphLawEquiv_marginal_toPMF (D : ExchangeableDigraphLaw) (k : ℕ) : PMF.map (⇑(finiteDigraphEquiv k)) (↑((exchangeableDigraphLawEquiv D).law.map ⋯)).toPMF = D.law k

The infinite directed law realizes the finite PMF-marginals: restricting the infinite law to the first k vertices, reading it as a probability mass function (Measure.toPMF, the finite carrier is countable) and transporting it across finiteDigraphEquiv recovers D.law k — the genuine PMF (Digraph (Fin k)), with no measurable structure placed on Digraph.