The evaluated exchangeable law of a kernel family (R4 sampler layer, #107)

The third R4 layer, on the merged evaluator (Graphon.RelKernelEvaluator): the i.i.d. uniform latent source over the global subset-latent indices, and the pushforward of that source through the RelKernelFamily evaluator — an exchangeable infinite relational law. The representation theorem (the converse: every dissociated exchangeable law arises this way) is deliberately not here; see issue #107 for its campaign plan.

• RelKernelFamily.eval — the evaluator over an arbitrary carrier V, agreeing definitionally with evalStructure on Vinfinite; its pullback transport eval_comap generalizes evalStructure_relabel to sortwise injections between carriers;
• RelSignature.latentSource — one i.i.d. [0,1]-uniform per nonempty finite set of sort-tagged vertices, with relabeling invariance latentSource_map_relabel (via LatentIndex.relabelEquiv and Measure.infinitePi_map_comp_equiv);
• RelKernelFamily.evalMeasure / RelKernelFamily.evalLaw — the evaluated law, packaged as an InfiniteRelExchangeableLaw: relabeling the structure is precomposing the source with the latent-index action (evalStructure_relabel), which preserves the source;
• RelKernelFamily.evalLaw_isDissociated — dissociation: disjoint vertex windows read disjoint collections of nonempty subset-latent indices (LatentIndex.map_ne_map_of_disjoint), so the i.i.d. source factorizes across the blocks (Measure.infinitePi_map_prodMk_of_disjoint); every finite restriction marginal is the same finite-block pushforward evalMeasure_map_restrict, independently of the injection.

The evaluator over an arbitrary carrier

noncomputable def RelSignature.RelCoord.latentWindow {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (η : S.LatentIndex V → ℝ) : PatternLatentIndex c.equalityPattern → ℝ

The local latent window over an arbitrary carrier: the latent source read through the coordinate's pattern-local indices — the arbitrary-carrier form of RelCoord.localLatents (definitionally equal to it on Vinfinite).

Equations

• c.latentWindow η A = η ((RelSignature.patternLatentIndexEquivCoord c) A).toLatentIndex

theorem RelSignature.RelCoord.latentWindow_eq_localLatents {S : RelSignature} (c : S.RelCoord S.Vinfinite) (ω : S.LatentIndex S.Vinfinite → ℝ) : c.latentWindow ω = c.localLatents ω

On the infinite carrier the general window is the evaluator layer's localLatents.

noncomputable def RelSignature.RelKernelFamily.eval {S : RelSignature} {V : S.Srt → Type u_1} (F : S.RelKernelFamily) (η : S.LatentIndex V → ℝ) : S.RelStructure V

The evaluated structure over an arbitrary carrier: each coordinate is its kernel applied to its local latent window.

Equations

• F.eval η c = F.toFun c.fst c.equalityPattern (c.latentWindow η)

theorem RelSignature.RelKernelFamily.eval_eq_evalStructure {S : RelSignature} (F : S.RelKernelFamily) : F.eval = F.evalStructure

On the infinite carrier the general evaluator is evalStructure (definitional).

theorem RelSignature.RelKernelFamily.measurable_eval {S : RelSignature} {V : S.Srt → Type u_1} (F : S.RelKernelFamily) : Measurable F.eval

The general evaluator is measurable in the latent source.

theorem RelSignature.RelCoord.latentWindow_map {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {f : (s : S.Srt) → V s → W s} (hf : ∀ (s : S.Srt), Function.Injective (f s)) (c : S.RelCoord V) (η : S.LatentIndex W → ℝ) (A' : PatternLatentIndex (map f c).equalityPattern) : (map f c).latentWindow η A' = c.latentWindow (fun (A : S.LatentIndex V) => η (LatentIndex.map f A)) ((PatternLatentIndex.congr ⋯) A')

The local latent window transports along sortwise injections: the window of the mapped coordinate is the window of the original coordinate, read off the source precomposed with the global latent-index action, at the transported block-set — the arbitrary-carrier generalization of RelCoord.localLatents_map.

theorem RelSignature.RelKernelFamily.eval_comap {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {f : (s : S.Srt) → V s → W s} (hf : ∀ (s : S.Srt), Function.Injective (f s)) (F : S.RelKernelFamily) (η : S.LatentIndex W → ℝ) : RelStructure.comap f (F.eval η) = F.eval fun (A : S.LatentIndex V) => η (LatentIndex.map f A)

Pullback commutes with evaluation: pulling the evaluated structure back along a sortwise injective family is evaluating at the source precomposed with the latent-index action — the arbitrary-carrier generalization of evalStructure_relabel, covering both relabelings and finite restrictions.

The latent source and the evaluated law

noncomputable def RelSignature.latentSource (S : RelSignature) : MeasureTheory.Measure (S.LatentIndex S.Vinfinite → ℝ)

The global latent source: one i.i.d. [0,1]-uniform per nonempty finite set of sort-tagged vertices — the randomness the dissociated functional representation consumes.

Equations

• S.latentSource = MeasureTheory.iidUniformSource (S.LatentIndex S.Vinfinite)

instance RelSignature.instIsProbabilityMeasureForallLatentIndexVinfiniteRealLatentSource {S : RelSignature} : MeasureTheory.IsProbabilityMeasure S.latentSource

theorem RelSignature.latentSource_map_relabel {S : RelSignature} (σ : S.Srt → Equiv.Perm ℕ) : MeasureTheory.Measure.map (fun (ω : S.LatentIndex S.Vinfinite → ℝ) (A : S.LatentIndex fun (s : S.Srt) => ℕ) => ω (LatentIndex.map (fun (s : S.Srt) => ⇑(σ s)) A)) S.latentSource = S.latentSource

Relabeling invariance of the latent source: precomposition with the latent-index action of a sortwise permutation family preserves the i.i.d. source — the action is a bijection of the index set (LatentIndex.relabelEquiv), and i.i.d. products are invariant under index bijections.

noncomputable def RelSignature.RelKernelFamily.evalMeasure {S : RelSignature} (F : S.RelKernelFamily) : MeasureTheory.Measure (S.RelStructure S.Vinfinite)

The evaluated measure of a kernel family: the latent source pushed through the evaluator.

Equations

• F.evalMeasure = MeasureTheory.Measure.map F.evalStructure S.latentSource

instance RelSignature.instIsProbabilityMeasureRelStructureVinfiniteEvalMeasure {S : RelSignature} (F : S.RelKernelFamily) : MeasureTheory.IsProbabilityMeasure F.evalMeasure

theorem RelSignature.RelKernelFamily.evalMeasure_map_relabel {S : RelSignature} (F : S.RelKernelFamily) (σ : S.Srt → Equiv.Perm ℕ) : MeasureTheory.Measure.map (RelStructure.relabel σ) F.evalMeasure = F.evalMeasure

Exchangeability of the evaluated measure: relabeling the evaluated structure is precomposing the latent source with the latent-index action (evalStructure_relabel), and the source is invariant under that action (latentSource_map_relabel).

noncomputable def RelSignature.RelKernelFamily.evalLaw {S : RelSignature} (F : S.RelKernelFamily) : S.InfiniteRelExchangeableLaw

The evaluated exchangeable law of a kernel family — the forward half of the dissociated functional Aldous–Hoover–Kallenberg representation.

Equations

• F.evalLaw = { law := ⟨F.evalMeasure, ⋯⟩, exchangeable := ⋯ }

@[simp]

theorem RelSignature.RelKernelFamily.evalLaw_law {S : RelSignature} (F : S.RelKernelFamily) : ↑F.evalLaw.law = F.evalMeasure

Dissociation of the evaluated law

@[implicit_reducible]

noncomputable instance RelSignature.instFintypeLatentIndexVfinite {S : RelSignature} [Fintype S.Srt] (n : S.Srt → ℕ) : Fintype (S.LatentIndex (Vfinite n))

Latent indices over a finite carrier form a finite type — the two blocks of the dissociation pair each read a finite latent window.

Equations

• RelSignature.instFintypeLatentIndexVfinite n = Subtype.fintype Finset.Nonempty

theorem RelSignature.RelKernelFamily.evalMeasure_map_restrict {S : RelSignature} [Fintype S.Srt] (F : S.RelKernelFamily) {n : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ ℕ) : MeasureTheory.Measure.map (RelStructure.restrict e) F.evalMeasure = MeasureTheory.Measure.map F.eval (MeasureTheory.Measure.pi fun (x : S.LatentIndex (Vfinite n)) => MeasureTheory.uniform01)

Every finite sortwise-injective restriction of the evaluated measure is the same finite-block pushforward — independently of the injection: restriction commutes with evaluation (eval_comap), and the precomposed source projects to the i.i.d. finite latent block (Measure.infinitePi_map_comp_of_injective).

theorem RelSignature.RelKernelFamily.evalMeasure_map_blockPair {S : RelSignature} [Fintype S.Srt] (F : S.RelKernelFamily) (k l : S.Srt → ℕ) : MeasureTheory.Measure.map (blockPair k l) F.evalMeasure = (MeasureTheory.Measure.map (RelStructure.restrictFin k) F.evalMeasure).prod (MeasureTheory.Measure.map (RelStructure.restrictFin l) F.evalMeasure)

The joint block law of the evaluated measure factorizes: the two vertex windows are disjoint, so the nonempty subset-latent collections they read are disjoint (LatentIndex.map_ne_map_of_disjoint), and the i.i.d. source splits into a product across them (Measure.infinitePi_map_prodMk_of_disjoint).

theorem RelSignature.RelKernelFamily.evalLaw_isDissociated {S : RelSignature} [Fintype S.Srt] (F : S.RelKernelFamily) : F.evalLaw.IsDissociated

The evaluated law is dissociated — disjoint vertex windows read disjoint collections of nonempty subset-latent indices, and the i.i.d. latent source factorizes across them. With exchangeability (evalLaw), this completes the forward half of the dissociated functional Aldous–Hoover–Kallenberg representation.