Digraphons: the five-component CAF directed graphon (directed umbrella #84, D3a / #87)

The measure-theoretic limit object for directed graphs (Diaconis–Janson §9, Cai–Ackerman–Freer). A general digraphon is not a single asymmetric kernel A(x,y): reciprocal edges may be dependent. The correct object assigns to each ordered pair a probability distribution over the four reciprocal-edge states (G i j, G j i) ∈ {0,1}², with a transpose symmetry, plus a {0,1}-valued loop coordinate.

Source crosswalk. Cai–Ackerman–Freer Definition 2.1 presents a digraphon as pointwise [0,1]-valued functions on [0,1]² (a genuine everywhere-defined probability vector at every point). This formalization generalizes the domain to an arbitrary measured space (α, μ) and stores the kernels modulo a.e. equality (as AEEqFun), which is the quotient-friendly form the exchangeable-law theory produces; simplexRep then reconstructs an everywhere-valid sampling representative, recovering the source's pointwise probability-vector property (needed to make the categorical sampler a genuine function on all of [0,1]).

• Digraphon α μ — the structure: four pair kernels pairProb a b : α × α →ₘ[μ.prod μ] ℝ (a, b : Bool the two directed-edge states) that are a.e. nonnegative, sum to one a.e., and satisfy the a.e. transpose law pairProb a b (y,x) = pairProb b a (x,y), plus a Bool-valued loop loop : α →ₘ[μ] Bool; with Digraphon.ext;
• Digraphon.pairRep / Digraphon.loopRep — genuine (everywhere-defined) measurable representatives of the pair kernels and the loop coordinate;
• Digraphon.pairSym — the transpose-symmetrized representative q a b (x,y) = ½(r a b (x,y) + r b a (y,x)), which satisfies transpose compatibility everywhere and agrees a.e. with pairProb;
• Digraphon.simplexRep — the everywhere-valid 3-simplex representative: pairSym where it is a genuine probability vector, and the fixed atom δ₀₀ elsewhere. It is measurable, nonnegative everywhere, sums to one everywhere, transpose-compatible everywhere, and equal a.e. to pairProb — the prerequisite for a well-defined categorical sampler (D3b).

No random sources / sampler / law here — that is D3b onward.

structure MeasureTheory.Digraphon (α : Type u_2) [MeasurableSpace α] (μ : Measure α) : Type u_2

A digraphon (five-component CAF directed graphon): four reciprocal-edge pair kernels pairProb a b : α × α →ₘ[μ.prod μ] ℝ (a, b : Bool the states of the two directed edges i → j, j → i) that a.e. form a probability vector on {0,1}² and satisfy the transpose law, together with a {0,1}-valued loop coordinate.

• pairProb : Bool → Bool → α × α →ₘ[μ.prod μ] ℝ

  The conditional probability that (G i j, G j i) = (a, b).

• ae_nonneg (a b : Bool) : ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ ↑(self.pairProb a b) p

  Each pair kernel is a.e. nonnegative.

• ae_sum_eq_one : ∀ᵐ (p : α × α) ∂μ.prod μ, ∑ a : Bool, ∑ b : Bool, ↑(self.pairProb a b) p = 1

  The four values sum to one a.e.

• transpose_ae (a b : Bool) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑(self.pairProb a b) p.swap = ↑(self.pairProb b a) p

  Transpose law: swapping the pair transposes the reciprocal-edge state, a.e.

• loop : α →ₘ[μ] Bool

  The {0,1}-valued loop coordinate.

theorem MeasureTheory.Digraphon.ext {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {W₁ W₂ : Digraphon α μ} (hp : ∀ (a b : Bool), W₁.pairProb a b = W₂.pairProb a b) (hl : W₁.loop = W₂.loop) : W₁ = W₂

theorem MeasureTheory.Digraphon.ext_iff {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {W₁ W₂ : Digraphon α μ} : W₁ = W₂ ↔ (∀ (a b : Bool), W₁.pairProb a b = W₂.pairProb a b) ∧ W₁.loop = W₂.loop

Measurable representatives

noncomputable def MeasureTheory.Digraphon.pairRep {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : α × α → ℝ

A genuine (everywhere-defined) measurable representative of the (a, b) pair kernel.

Equations

• W.pairRep a b = ↑(W.pairProb a b)

theorem MeasureTheory.Digraphon.measurable_pairRep {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : Measurable (W.pairRep a b)

noncomputable def MeasureTheory.Digraphon.loopRep {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) : α → Bool

A genuine (everywhere-defined) measurable representative of the loop coordinate.

Equations

• W.loopRep = ↑W.loop

theorem MeasureTheory.Digraphon.measurable_loopRep {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) : Measurable W.loopRep

The transpose-symmetrized representative

noncomputable def MeasureTheory.Digraphon.pairSym {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : α × α → ℝ

The transpose-symmetrized representative q a b (x, y) = ½(r a b (x, y) + r b a (y, x)).

Equations

• W.pairSym a b p = (W.pairRep a b p + W.pairRep b a p.swap) / 2

theorem MeasureTheory.Digraphon.measurable_pairSym {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : Measurable (W.pairSym a b)

@[simp]

theorem MeasureTheory.Digraphon.pairSym_swap {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) (p : α × α) : W.pairSym a b p.swap = W.pairSym b a p

Transpose compatibility of the symmetrized kernel, everywhere.

theorem MeasureTheory.Digraphon.pairSym_ae_eq {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : W.pairSym a b =ᵐ[μ.prod μ] ↑(W.pairProb a b)

The symmetrized kernel agrees a.e. with the given pair kernel (uses the a.e. transpose law).

The everywhere-valid 3-simplex representative

def MeasureTheory.Digraphon.IsValidAt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : Prop

Whether the symmetrized values at p form a genuine probability vector.

Equations

• W.IsValidAt p = ((∀ (a b : Bool), 0 ≤ W.pairSym a b p) ∧ ∑ a : Bool, ∑ b : Bool, W.pairSym a b p = 1)

theorem MeasureTheory.Digraphon.measurableSet_isValidAt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) : MeasurableSet {p : α × α | W.IsValidAt p}

theorem MeasureTheory.Digraphon.isValidAt_swap {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : W.IsValidAt p.swap ↔ W.IsValidAt p

Validity is invariant under swapping the pair.

noncomputable def MeasureTheory.Digraphon.simplexRep {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : α × α → ℝ

The everywhere-defined 3-simplex representative: the symmetrized kernel where it is a genuine probability vector, and the fixed atom δ₀₀ (all mass on (0,0)) elsewhere.

Equations

• W.simplexRep a b p = if W.IsValidAt p then W.pairSym a b p else if a = false ∧ b = false then 1 else 0

theorem MeasureTheory.Digraphon.measurable_simplexRep {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : Measurable (W.simplexRep a b)

theorem MeasureTheory.Digraphon.simplexRep_nonneg {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) (p : α × α) : 0 ≤ W.simplexRep a b p

Nonnegativity everywhere.

theorem MeasureTheory.Digraphon.simplexRep_sum_eq_one {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : ∑ a : Bool, ∑ b : Bool, W.simplexRep a b p = 1

The four values sum to one everywhere.

@[simp]

theorem MeasureTheory.Digraphon.simplexRep_swap {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) (p : α × α) : W.simplexRep a b p.swap = W.simplexRep b a p

Transpose compatibility everywhere.

theorem MeasureTheory.Digraphon.simplexRep_ae_eq {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (a b : Bool) : W.simplexRep a b =ᵐ[μ.prod μ] ↑(W.pairProb a b)

Agreement a.e. with the given pair kernels. On a conull set the symmetrized values are a valid probability vector, where simplexRep reduces to pairSym, which agrees a.e. with pairProb.