Special-family digraphon constructors (directed umbrella #84, D3c / #87)

The three classical special families of Cai–Ackerman–Freer (Priors on exchangeable directed graphs, arXiv:1510.08440), realized as digraphons — each is a choice of the four reciprocal-edge probabilities. Source crosswalk: digraphons and their sampling are CAF §2.3–2.4; the asymmetric-function model is CAF §3.1; undirected graphs and tournaments are CAF §3.2.1–3.2.2.

• Digraphon.ofFun — the generic builder from four measurable pointwise kernels satisfying the digraphon axioms a.e., with the a.e. compatibility lemmas ofFun_pairProb_ae / ofFun_simplexRep_ae;
• Digraphon.ofGraphon W — the ordinary-graphon embedding: reciprocal edges fully correlated (p₁₁ = W, p₀₀ = 1 − W, no antisymmetric mass, no loops) — an undirected graph seen as a digraph;
• Digraphon.ofTournament A — the tournament digraphon: exactly one direction per pair (p₁₀ = A, p₀₁ = A ∘ swap, p₁₁ = p₀₀ = 0, no loops), from an orientation kernel with A p + A p.swap = 1 a.e.;
• Digraphon.ofKernel A L — the asymmetric-kernel digraphon: the two directions drawn independently (p_{ab} = A^a (1−A)^{1−a} · (A∘swap)^b (1−A∘swap)^{1−b}, all four products genuinely present), with an arbitrary loop coordinate L.

Each constructor comes with the a.e. identification of its four pair kernels (ofGraphon_pairProb_ae / ofTournament_pairProb_ae / ofKernel_pairProb_ae), from which the simplexRep-level compatibility is inherited via Digraphon.simplexRep_ae_eq. The sampler/law identification for each family is the D3c follow-up.

The generic pointwise builder

noncomputable def MeasureTheory.Digraphon.ofFun {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (f : Bool → Bool → α × α → ℝ) (hmeas : ∀ (a b : Bool), Measurable (f a b)) (hnn : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ f a b p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ∑ a : Bool, ∑ b : Bool, f a b p = 1) (htr : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, f a b p.swap = f b a p) (L : α → Bool) (hL : Measurable L) : Digraphon α μ

The generic digraphon builder from four measurable pointwise kernels satisfying the digraphon axioms almost everywhere, together with a measurable loop coordinate.

Equations

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

theorem MeasureTheory.Digraphon.ofFun_pairProb_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (f : Bool → Bool → α × α → ℝ) (hmeas : ∀ (a b : Bool), Measurable (f a b)) (hnn : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ f a b p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ∑ a : Bool, ∑ b : Bool, f a b p = 1) (htr : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, f a b p.swap = f b a p) (L : α → Bool) (hL : Measurable L) (a b : Bool) : ↑((ofFun f hmeas hnn hsum htr L hL).pairProb a b) =ᵐ[μ.prod μ] f a b

The pair kernels of ofFun are (a.e.) the given pointwise kernels.

theorem MeasureTheory.Digraphon.ofFun_loop_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (f : Bool → Bool → α × α → ℝ) (hmeas : ∀ (a b : Bool), Measurable (f a b)) (hnn : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ f a b p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ∑ a : Bool, ∑ b : Bool, f a b p = 1) (htr : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, f a b p.swap = f b a p) (L : α → Bool) (hL : Measurable L) : ↑(ofFun f hmeas hnn hsum htr L hL).loop =ᵐ[μ] L

The loop coordinate of ofFun is (a.e.) the given pointwise loop.

theorem MeasureTheory.Digraphon.ofFun_simplexRep_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (f : Bool → Bool → α × α → ℝ) (hmeas : ∀ (a b : Bool), Measurable (f a b)) (hnn : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ f a b p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ∑ a : Bool, ∑ b : Bool, f a b p = 1) (htr : ∀ (a b : Bool), ∀ᵐ (p : α × α) ∂μ.prod μ, f a b p.swap = f b a p) (L : α → Bool) (hL : Measurable L) (a b : Bool) : (ofFun f hmeas hnn hsum htr L hL).simplexRep a b =ᵐ[μ.prod μ] f a b

The simplexRep of ofFun agrees a.e. with the given pointwise kernels — the simplexRep-level compatibility all three special families inherit.

The ordinary-graphon embedding

noncomputable def MeasureTheory.Digraphon.ofGraphon {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (W : Graphon α μ) : Digraphon α μ

The ordinary-graphon embedding: the digraphon whose reciprocal-edge distribution puts mass W (x, y) on the doubly-present state and 1 − W (x, y) on the doubly-absent state — an undirected graph viewed as a digraph, with no loops.

Equations

• MeasureTheory.Digraphon.ofGraphon W = MeasureTheory.Digraphon.ofFun (MeasureTheory.Digraphon.graphonFour✝ W) ⋯ ⋯ ⋯ ⋯ (fun (x : α) => false) ⋯

theorem MeasureTheory.Digraphon.ofGraphon_pairProb_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (W : Graphon α μ) : ↑((ofGraphon W).pairProb true true) =ᵐ[μ.prod μ] ↑W.toAEEqFun ∧ (↑((ofGraphon W).pairProb false false) =ᵐ[μ.prod μ] fun (p : α × α) => 1 - ↑W.toAEEqFun p) ∧ ↑((ofGraphon W).pairProb true false) =ᵐ[μ.prod μ] 0 ∧ ↑((ofGraphon W).pairProb false true) =ᵐ[μ.prod μ] 0

The four pair kernels of the graphon embedding, a.e.: p₁₁ = W, p₀₀ = 1 − W, and no antisymmetric mass.

theorem MeasureTheory.Digraphon.ofGraphon_simplexRep_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (W : Graphon α μ) : (ofGraphon W).simplexRep true true =ᵐ[μ.prod μ] ↑W.toAEEqFun ∧ ((ofGraphon W).simplexRep false false =ᵐ[μ.prod μ] fun (p : α × α) => 1 - ↑W.toAEEqFun p) ∧ (ofGraphon W).simplexRep true false =ᵐ[μ.prod μ] 0 ∧ (ofGraphon W).simplexRep false true =ᵐ[μ.prod μ] 0

The simplexRep of the graphon embedding, a.e.

theorem MeasureTheory.Digraphon.ofGraphon_loop_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (W : Graphon α μ) : ↑(ofGraphon W).loop =ᵐ[μ] fun (x : α) => false

The graphon embedding carries no loops (a.e.).

The tournament digraphon

noncomputable def MeasureTheory.Digraphon.ofTournament {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hnn : ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ ↑A p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p + ↑A p.swap = 1) : Digraphon α μ

The tournament digraphon: almost everywhere, exactly one of the two directed edges is present — p₁₀ = A, p₀₁ = A ∘ swap, no doubly-present or doubly-absent mass, no loops — from an orientation kernel A with A p + A p.swap = 1 a.e. (Since hsum holds only a.e., simplexRep may take its δ₀₀ fallback on an exceptional null set of latent pairs; the sampled digraph is a tournament almost surely, not pointwise in the latents.)

Equations

• MeasureTheory.Digraphon.ofTournament A hnn hsum = MeasureTheory.Digraphon.ofFun (MeasureTheory.Digraphon.tournamentFour✝ A) ⋯ ⋯ ⋯ ⋯ (fun (x : α) => false) ⋯

theorem MeasureTheory.Digraphon.ofTournament_pairProb_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hnn : ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ ↑A p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p + ↑A p.swap = 1) : ↑((ofTournament A hnn hsum).pairProb true false) =ᵐ[μ.prod μ] ↑A ∧ (↑((ofTournament A hnn hsum).pairProb false true) =ᵐ[μ.prod μ] fun (p : α × α) => ↑A p.swap) ∧ ↑((ofTournament A hnn hsum).pairProb true true) =ᵐ[μ.prod μ] 0 ∧ ↑((ofTournament A hnn hsum).pairProb false false) =ᵐ[μ.prod μ] 0

The four pair kernels of the tournament digraphon, a.e.

theorem MeasureTheory.Digraphon.ofTournament_simplexRep_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hnn : ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ ↑A p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p + ↑A p.swap = 1) : (ofTournament A hnn hsum).simplexRep true false =ᵐ[μ.prod μ] ↑A ∧ ((ofTournament A hnn hsum).simplexRep false true =ᵐ[μ.prod μ] fun (p : α × α) => ↑A p.swap) ∧ (ofTournament A hnn hsum).simplexRep true true =ᵐ[μ.prod μ] 0 ∧ (ofTournament A hnn hsum).simplexRep false false =ᵐ[μ.prod μ] 0

The simplexRep of the tournament digraphon, a.e.

theorem MeasureTheory.Digraphon.ofTournament_loop_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hnn : ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ ↑A p) (hsum : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p + ↑A p.swap = 1) : ↑(ofTournament A hnn hsum).loop =ᵐ[μ] fun (x : α) => false

The tournament digraphon carries no loops (a.e.).

The asymmetric-kernel digraphon

noncomputable def MeasureTheory.Digraphon.ofKernel {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hmem : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p ∈ Set.Icc 0 1) (L : α → Bool) (hL : Measurable L) : Digraphon α μ

The asymmetric-kernel digraphon: the two directed edges of a pair are drawn independently — p_{ab} (x, y) is the product of the a-mass of A (x, y) and the b-mass of A (y, x), so all four reciprocal-edge products are genuinely present — with an arbitrary loop coordinate L.

Equations

• MeasureTheory.Digraphon.ofKernel A hmem L hL = MeasureTheory.Digraphon.ofFun (MeasureTheory.Digraphon.kernelFour✝ A) ⋯ ⋯ ⋯ ⋯ L hL

theorem MeasureTheory.Digraphon.ofKernel_pairProb_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hmem : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p ∈ Set.Icc 0 1) (L : α → Bool) (hL : Measurable L) (a b : Bool) : ↑((ofKernel A hmem L hL).pairProb a b) =ᵐ[μ.prod μ] fun (p : α × α) => (if a = true then ↑A p else 1 - ↑A p) * if b = true then ↑A p.swap else 1 - ↑A p.swap

The four pair kernels of the asymmetric-kernel digraphon, a.e.: the independent products.

theorem MeasureTheory.Digraphon.ofKernel_simplexRep_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hmem : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p ∈ Set.Icc 0 1) (L : α → Bool) (hL : Measurable L) (a b : Bool) : (ofKernel A hmem L hL).simplexRep a b =ᵐ[μ.prod μ] fun (p : α × α) => (if a = true then ↑A p else 1 - ↑A p) * if b = true then ↑A p.swap else 1 - ↑A p.swap

The simplexRep of the asymmetric-kernel digraphon, a.e.: the independent products.

theorem MeasureTheory.Digraphon.ofKernel_loop_ae {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SFinite μ] (A : α × α →ₘ[μ.prod μ] ℝ) (hmem : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑A p ∈ Set.Icc 0 1) (L : α → Bool) (hL : Measurable L) : ↑(ofKernel A hmem L hL).loop =ᵐ[μ] L

The loop coordinate of the asymmetric-kernel digraphon, a.e.