The categorical outcome and explicit sampler of a digraphon (#84, D3b steps 2–3 / #87)

The reciprocal-edge outcome of a digraphon at a fixed pair is a single categorical draw over the four states (G i j, G j i) ∈ {0,1}², carrying all four probabilities — not two independent Bernoullis. This file builds that mechanism from the everywhere-valid simplexRep, then the explicit finite and infinite digraph samplers on top of it:

• Digraphon.pairPMF p — the four-state distribution at p, a PMF (Bool × Bool) with mass ENNReal.ofReal (simplexRep a b p) on (a, b);

• Digraphon.catOutcome p — the one-uniform categorical map: partition [0,1] by the four probabilities and read off the reciprocal-edge state from a single uniform;

• Digraphon.uniform01_map_catOutcome — the exact four-state law: the pushforward of the uniform measure under catOutcome p is exactly pairPMF p;

• Digraphon.samplerSource μ — the sampler source: i.i.d. vertex positions (law μ) and one [0,1]-uniform per off-diagonal unordered pair (OffDiagPairIndex ℕ), independent;

• Digraphon.sampleAdj — the sampler's adjacency bit at an ordered pair, in the natural-number order: the diagonal reads the loop coordinate; an off-diagonal pair reads one coordinate of the single categorical draw at the increasing-order positions from the one uniform of the unordered pair (sampleAdj_self / sampleAdj_of_lt / sampleAdj_of_gt);

• Digraphon.sampleInfinite / Digraphon.sampleFinite n — the explicit infinite sampler (into InfiniteDigraph) and its restriction to the first n vertices, both measurable in the sources.

• Digraphon.samplerSource_forall_sampleAdj — the exact finite-event product formula (steps 4–5), over an arbitrary injective labeling: one loop indicator per vertex and one simplexRep mass per unordered pair, with a labeling-free right-hand side;

• Digraphon.sampleRelLaw / Digraphon.sampleDigraphLaw — the sampled exchangeable law (consistency from the labeling-free formula), and Digraphon.map_sampleInfinite / map_sampleInfinite_eq_equiv_law — the sampler realizes its infinite law, identified through exchangeableDigraphLawEquiv (D2);

• Digraphon.map_sampleInfinite_relabel / Digraphon.map_sampleFinite_pair_disjoint — exchangeability and dissociation of the sampled law.

The generic i.i.d. sources (MeasureTheory.uniform01, iidVertexSource, iidUniformSource) are reused from Graphon.SamplerSources. Next: D3c (ordinary-graphon / tournament / asymmetric-kernel constructors).

The four-state distribution

noncomputable def MeasureTheory.Digraphon.pairPMF {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : PMF (Bool × Bool)

The four-state reciprocal-edge distribution at a pair p, as a PMF (Bool × Bool).

Equations

• W.pairPMF p = PMF.ofFintype (fun (ab : Bool × Bool) => ENNReal.ofReal (W.simplexRep ab.1 ab.2 p)) ⋯

@[simp]

theorem MeasureTheory.Digraphon.pairPMF_apply {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) (ab : Bool × Bool) : (W.pairPMF p) ab = ENNReal.ofReal (W.simplexRep ab.1 ab.2 p)

theorem MeasureTheory.Digraphon.pairPMF_swap {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : W.pairPMF p.swap = PMF.map Prod.swap (W.pairPMF p)

Distributional transpose equivariance: swapping the pair transposes the four-state distribution. (Pointwise equivariance of catOutcome is neither true nor needed; this distributional form — cashing out simplexRep_swap — is the statement that handles orientation reversal under relabeling, or any alternate ordering of an unordered pair.)

The one-uniform categorical outcome

noncomputable def MeasureTheory.Digraphon.catOutcome {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) (u : ℝ) : Bool × Bool

The one-uniform categorical map: partition [0,1] into four sub-intervals of lengths simplexRep (0,0), simplexRep (0,1), simplexRep (1,0), simplexRep (1,1) and read the reciprocal-edge state off a single uniform value.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Digraphon.measurable_catOutcome_joint {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) : Measurable fun (z : (α × α) × ℝ) => W.catOutcome z.1 z.2

Joint measurability of the categorical outcome in both the pair and the uniform — the form the sampler needs, since it evaluates catOutcome at p = (Uᵢ, Uⱼ) varying with the sample. Each threshold is a simplexRep of the pair coordinate, compared with the uniform coordinate.

theorem MeasureTheory.Digraphon.measurable_catOutcome {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : Measurable (W.catOutcome p)

Measurability of the categorical outcome at a fixed pair — a corollary of the joint version.

The exact four-state law

theorem MeasureTheory.Digraphon.uniform01_map_catOutcome {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) : Measure.map (W.catOutcome p) uniform01 = (W.pairPMF p).toMeasure

The exact four-state law: the pushforward of the uniform measure under the one-uniform categorical map is exactly the four-state distribution pairPMF p.

theorem MeasureTheory.Digraphon.uniform01_catOutcome_singleton {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (p : α × α) (ab : Bool × Bool) : uniform01 {u : ℝ | W.catOutcome p u = ab} = ENNReal.ofReal (W.simplexRep ab.1 ab.2 p)

The exact single-event factor consumed by the product-law proof: the uniform mass of the event that the categorical outcome equals ab is exactly simplexRep ab.

The sampler source

noncomputable def MeasureTheory.Digraphon.samplerSource {α : Type u_1} [MeasurableSpace α] (μ : Measure α) : Measure ((ℕ → α) × (OffDiagPairIndex ℕ → ℝ))

The digraph sampler source: i.i.d. vertex positions with law μ and one [0,1]-uniform per off-diagonal unordered pair, independent.

Equations

• MeasureTheory.Digraphon.samplerSource μ = (MeasureTheory.iidVertexSource μ).prod (MeasureTheory.iidUniformSource (OffDiagPairIndex ℕ))

instance MeasureTheory.Digraphon.instIsProbabilityMeasureProdForallNatForallOffDiagPairIndexRealSamplerSource {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ] : IsProbabilityMeasure (samplerSource μ)

The explicit sampler (D3b step 3)

noncomputable def MeasureTheory.Digraphon.sampleAdj {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) (i j : ℕ) : Bool

The sampler's adjacency bit at an ordered pair (i, j), in the natural-number order: the diagonal reads the loop coordinate at the vertex position; an off-diagonal pair reads one coordinate of the single categorical draw at the increasing-order positions — for i < j the first coordinate of catOutcome (xᵢ, xⱼ), for j < i the second coordinate of catOutcome (xⱼ, xᵢ) — from the one uniform attached to the unordered pair {i, j}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.Digraphon.sampleAdj_self {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) (i : ℕ) : W.sampleAdj ω i i = W.loopRep (ω.1 i)

The diagonal coordinate of the sampler: the loop bit at the vertex position.

theorem MeasureTheory.Digraphon.sampleAdj_of_lt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) {i j : ℕ} (h : i < j) : W.sampleAdj ω i j = (W.catOutcome (ω.1 i, ω.1 j) (ω.2 (OffDiagPairIndex.mk ⋯))).1

The increasing-order coordinate of the sampler: for i < j, the first component of the categorical draw at (xᵢ, xⱼ).

theorem MeasureTheory.Digraphon.sampleAdj_of_gt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) {i j : ℕ} (h : j < i) : W.sampleAdj ω i j = (W.catOutcome (ω.1 j, ω.1 i) (ω.2 (OffDiagPairIndex.mk ⋯))).2

The decreasing-order coordinate of the sampler: for j < i, the second component of the categorical draw at (xⱼ, xᵢ) — the same draw as the (j, i) coordinate, giving the reciprocal-edge dependence.

theorem MeasureTheory.Digraphon.sampleAdj_pair_of_lt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) {i j : ℕ} (h : i < j) : (W.sampleAdj ω i j, W.sampleAdj ω j i) = W.catOutcome (ω.1 i, ω.1 j) (ω.2 (OffDiagPairIndex.mk ⋯))

The paired coordinates at an unordered pair are the single categorical draw: for i < j, the reciprocal-edge pair (sampleAdj ω i j, sampleAdj ω j i) is exactly catOutcome (xᵢ, xⱼ) at the pair's one uniform — the reciprocal dependence in one statement, the form the exact-event product formula consumes.

theorem MeasureTheory.Digraphon.measurable_sampleAdj {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (i j : ℕ) : Measurable fun (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) => W.sampleAdj ω i j

Measurability of the adjacency bit in the sources, at each fixed ordered pair — via the joint measurability of catOutcome, since the pair argument varies with the sample.

noncomputable def MeasureTheory.Digraphon.sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) : InfiniteDigraph

The explicit infinite digraph sampler: the relational structure whose ordered-pair coordinates are the sampler's adjacency bits.

Equations

• W.sampleInfinite ω c = W.sampleAdj ω (c.snd 0) (c.snd 1)

@[simp]

theorem MeasureTheory.Digraphon.adjBit_sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) (i j : ℕ) : (W.sampleInfinite ω).adjBit i j = W.sampleAdj ω i j

The adjacency bit of the sampled infinite digraph, unfolded.

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

The infinite digraph sampler is measurable in the sources: each ordered-pair coordinate is a measurable adjacency bit.

noncomputable def MeasureTheory.Digraphon.sampleFinite {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (n : ℕ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) : FiniteDigraph n

The finite digraph sampler: the restriction of the infinite sampler to the first n vertices.

Equations

• W.sampleFinite n ω = InfiniteDigraph.restrictFin n (W.sampleInfinite ω)

@[simp]

theorem MeasureTheory.Digraphon.sampleFinite_apply {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (n : ℕ) (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) (i j : Fin n) : W.sampleFinite n ω (digraphCoord i j) = W.sampleAdj ω ↑i ↑j

The ordered-pair coordinate of the sampled finite digraph, unfolded.

theorem MeasureTheory.Digraphon.measurable_sampleFinite {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) (n : ℕ) : Measurable (W.sampleFinite n)

The exact finite-event product formula (D3b step 4)

The probability that the sampler realizes exactly a target finite digraph, stated over an arbitrary injective labeling ι : Fin n → ℕ of the sampled vertices: the right-hand side does not depend on ι (transpose flips are absorbed by simplexRep_swap), which is precisely what makes restriction-consistency and exchangeability corollaries of this one computation.

noncomputable def MeasureTheory.Digraphon.sampleEventIntegrand {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) {n : ℕ} (D : FiniteDigraph n) (y : Fin n → α) : ENNReal

The exact-event integrand: the conditional probability, given vertex positions y, that the sampler realizes exactly the digraph D — one loop indicator per vertex and one simplexRep mass per unordered pair (the single categorical draw carrying both directed edges).

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Digraphon.measurable_sampleEventIntegrand {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) {n : ℕ} (D : FiniteDigraph n) : Measurable (W.sampleEventIntegrand D)

theorem MeasureTheory.Digraphon.samplerSource_forall_sampleAdj {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) {n : ℕ} {ι : Fin n → ℕ} [IsProbabilityMeasure μ] (hι : Function.Injective ι) (D : FiniteDigraph n) : (samplerSource μ) {ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ) | ∀ (i j : Fin n), W.sampleAdj ω (ι i) (ι j) = D (digraphCoord i j)} = ∫⁻ (y : Fin n → α), W.sampleEventIntegrand D y ∂Measure.pi fun (x : Fin n) => μ

The exact finite-event product formula (D3b step 4), over an arbitrary injective labeling ι of the sampled vertices: the probability that the sampler realizes exactly D on the labels ι is the integral, over i.i.d. μ-positions, of the loop indicators times one simplexRep mass per unordered pair. The right-hand side does not depend on ι — the source of consistency and exchangeability.

theorem MeasureTheory.Digraphon.samplerSource_sampleFinite_singleton {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) {n : ℕ} [IsProbabilityMeasure μ] (D : FiniteDigraph n) : (samplerSource μ) {ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ) | W.sampleFinite n ω = D} = ∫⁻ (y : Fin n → α), W.sampleEventIntegrand D y ∂Measure.pi fun (x : Fin n) => μ

The exact-event formula for the finite sampler: specialization of the product formula to the identity labeling — the mass the sampled digraph law puts on a single target D.

The sampled exchangeable law and the infinite identification (D3b step 5)

The ι-freedom of the product formula makes restriction-consistency immediate, so the finite sampler laws assemble into a RelExchangeableLaw digraphSig; the infinite sampler then realizes its (R2b) infinite law, by finite-restriction measure extensionality.

instance MeasureTheory.Digraphon.instIsProbabilityMeasureFiniteDigraphMapProdForallNatForallOffDiagPairIndexRealSampleFiniteSamplerSource {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] (k : ℕ) : IsProbabilityMeasure (Measure.map (W.sampleFinite k) (samplerSource μ))

theorem MeasureTheory.Digraphon.map_sampleFinite_restrict {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] {k l : ℕ} (e : Fin k ↪ Fin l) : Measure.map (RelSignature.RelStructure.restrict fun (x : Unit) => e) (Measure.map (W.sampleFinite l) (samplerSource μ)) = Measure.map (W.sampleFinite k) (samplerSource μ)

Restriction-consistency of the sampled finite laws: restricting the l-vertex sample along any injection e : Fin k ↪ Fin l reproduces the k-vertex sample law — both sides have the same exact-event masses by the labeling-free product formula.

noncomputable def MeasureTheory.Digraphon.sampleRelLaw {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] : digraphSig.RelExchangeableLaw

The sampled relational law: the finite sampler laws, packaged as an exchangeable relational law over digraphSig (consistency from the labeling-free product formula).

Equations

• W.sampleRelLaw = { marginal := fun (n : digraphSig.Srt → ℕ) => ⟨MeasureTheory.Measure.map (W.sampleFinite (n ())) (MeasureTheory.Digraphon.samplerSource μ), ⋯⟩, consistent := ⋯ }

@[simp]

theorem MeasureTheory.Digraphon.sampleRelLaw_marginal {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] (n : Unit → ℕ) : ↑(W.sampleRelLaw.marginal n) = Measure.map (W.sampleFinite (n ())) (samplerSource μ)

noncomputable def MeasureTheory.Digraphon.sampleDigraphLaw {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] : ExchangeableDigraphLaw

The sampled digraph law, in the user-facing PMF form of D2.

Equations

• W.sampleDigraphLaw = digraphLawEquiv.symm W.sampleRelLaw

@[simp]

theorem MeasureTheory.Digraphon.sampleDigraphLaw_law {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] (k : ℕ) : W.sampleDigraphLaw.law k = PMF.map (⇑(finiteDigraphEquiv k)) (Measure.map (W.sampleFinite k) (samplerSource μ)).toPMF

theorem MeasureTheory.Digraphon.map_sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] : Measure.map W.sampleInfinite (samplerSource μ) = ↑W.sampleRelLaw.infiniteLaw

The sampler realizes the infinite exchangeable law (D3b step 5): the pushforward of the sampler source under the infinite sampler is exactly the (R2b) infinite law of the sampled relational law — by finite-restriction measure extensionality, since the finite sampler is the restriction of the infinite sampler.

theorem MeasureTheory.Digraphon.map_sampleInfinite_eq_equiv_law {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] : Measure.map W.sampleInfinite (samplerSource μ) = ↑(exchangeableDigraphLawEquiv W.sampleDigraphLaw).law

The headline identification: the sampler's infinite law is the image of the sampled PMF-based digraph law under the directed finite/infinite equivalence exchangeableDigraphLawEquiv (D2).

Exchangeability and dissociation (D3b step 5, corollaries)

theorem MeasureTheory.Digraphon.map_sampleInfinite_relabel {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] (σ : Equiv.Perm ℕ) : Measure.map (RelSignature.RelStructure.relabel fun (x : Unit) => σ) (Measure.map W.sampleInfinite (samplerSource μ)) = Measure.map W.sampleInfinite (samplerSource μ)

Exchangeability of the sampler's law: invariance under every relabeling of ℕ — free from the identification with the infinite law, which is relabeling-invariant by R2c.

theorem MeasureTheory.Digraphon.samplerSource_inter_disjoint {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] {k l : ℕ} {ι₁ : Fin k → ℕ} {ι₂ : Fin l → ℕ} (hι₁ : Function.Injective ι₁) (hι₂ : Function.Injective ι₂) (hd : ∀ (i : Fin k) (j : Fin l), ι₁ i ≠ ι₂ j) (D₁ : FiniteDigraph k) (D₂ : FiniteDigraph l) : (samplerSource μ) ({ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ) | ∀ (i j : Fin k), W.sampleAdj ω (ι₁ i) (ι₁ j) = D₁ (digraphCoord i j)} ∩ {ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ) | ∀ (i j : Fin l), W.sampleAdj ω (ι₂ i) (ι₂ j) = D₂ (digraphCoord i j)}) = (samplerSource μ) {ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ) | ∀ (i j : Fin k), W.sampleAdj ω (ι₁ i) (ι₁ j) = D₁ (digraphCoord i j)} * (samplerSource μ) {ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ) | ∀ (i j : Fin l), W.sampleAdj ω (ι₂ i) (ι₂ j) = D₂ (digraphCoord i j)}

Independence over disjoint labels (dissociation, event form): the exact events of the sampler on two disjoint label sets are independent — conditionally on the positions the two events use disjoint uniform coordinates, and the position integral splits over the two blocks of the combined labeling.

theorem MeasureTheory.Digraphon.map_sampleFinite_pair_disjoint {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (W : Digraphon α μ) [IsProbabilityMeasure μ] (k l : ℕ) : Measure.map (fun (ω : (ℕ → α) × (OffDiagPairIndex ℕ → ℝ)) => (RelSignature.RelStructure.restrict (fun (x : Unit) => Fin.castAddEmb l) (W.sampleFinite (k + l) ω), RelSignature.RelStructure.restrict (fun (x : Unit) => Fin.natAddEmb k) (W.sampleFinite (k + l) ω))) (samplerSource μ) = (Measure.map (W.sampleFinite k) (samplerSource μ)).prod (Measure.map (W.sampleFinite l) (samplerSource μ))

Dissociation (distributional form): the restrictions of the (k + l)-vertex sample to the first k and the last l vertices are independent, with the k- and l-vertex sample laws as marginals — the sampled law is dissociated.