Functional Aldous–Hoover for dissociated laws (issue #64)

The dissociated/extreme case of the functional Aldous–Hoover theorem — classically equivalent to the ergodic case; the formal equivalence is issue #59 — needs no measurable selection: a raw representative is chosen only after the graphon class is fixed.

• InfiniteGraph.sampleInfinite_adj — the sampler's literal coordinates: X_{ij} = 1{U_{ij} ≤ W(U_i, U_j)} (one uniform per unordered pair, evaluated at the clamped representative and the Quot.out-canonical endpoint order);
• InfiniteGraph.isDissociated_iff_exists_sampler — an infinite exchangeable graph law is dissociated iff it is the law of the explicit W-random infinite graph for some raw graphon W — extremality collapses the mixing measure to one class, and the explicit sampler realizes that single fiber.

theorem InfiniteGraph.sampleInfinite_adj {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (ω : (ℕ → α) × (EdgeIndex → ℝ)) {i j : ℕ} (hij : i ≠ j) : (sampleInfinite W ω).Adj i j ↔ ω.2 ⟨s(i, j), ⋯⟩ ≤ clampedRep W (ω.1 (Quot.out s(i, j)).1, ω.1 (Quot.out s(i, j)).2)

The sampler's adjacency, in the literal functional Aldous–Hoover form: distinct vertices i, j are adjacent exactly when the pair's uniform falls below the (clamped) graphon value at the latent positions.

theorem InfiniteGraph.isDissociated_iff_exists_sampler {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (M : Graphon.InfiniteExchangeableGraphLaw) : M.IsDissociated ↔ ∃ (W : Graphon α μ), MeasureTheory.Measure.map (sampleInfinite W) (samplerSource μ) = ↑M.law

Functional Aldous–Hoover for dissociated laws (issue #64, the dissociated/ extreme case; classically equivalent to ergodic — formalized in issue #59): an infinite exchangeable graph law is dissociated iff it is the law of the explicit W-random infinite graph X_{ij} = 1{U_{ij} ≤ W(U_i, U_j)} for some raw graphon W. No measurable selection in the class variable is needed: extremality fixes a single graphon class, and a representative is chosen for that one class.

theorem InfiniteGraph.exists_sampler_of_isDissociated {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {M : Graphon.InfiniteExchangeableGraphLaw} (hM : M.IsDissociated) : ∃ (W : Graphon α μ), MeasureTheory.Measure.map (sampleInfinite W) (samplerSource μ) = ↑M.law

The source-map law equality for a dissociated law: extract the realizing raw graphon.