The pooled rank extension (R4 converse, #107) #

Stage 2 of the pooled-latent extension gate: the joint object carrying a genuine mixed action on both the structure and the latents.

PooledRankExtension C has exactly three fields — the joint law on the pooled structure space times the pooled latent cube, the exact restriction of that law to C.P along the two original restrictions, and invariance under the full pooled permutation family. There is no independence field: an independent pool would recreate the defect of the rejected factor coupling, and nothing here needs one.

RankRepresentation.pooledExtension is the cheap constructor. Both of its laws come from the joint self-injection invariance theorem RankRepresentation.map_prodMap_restrict_self, through the bridges of Graphon.RelPooledLatents:

writing pv for poolVertexEquiv and ov for originalVertex, the transport is comap pv on structures and restriction along pv on latents;
restrictOriginal ∘ transport is comap (pv ∘ ov), and pv ∘ ov is a self-injection of the original carrier — that is map_restrictOriginal;
relabel ρ ∘ transport = transport ∘ relabel κ for the conjugate κ = pv ∘ ρ ∘ pv⁻¹, a permutation of the original carrier — that is invariant, for every mixed ρ, since a permutation is in particular an injection.

The structure deliberately carries no mixed-window field: the joint mixed-window marginal, and current-rank recovery and screening on mixed pooled supports, are separate derived consequences of these three fields rather than part of the primitive. Nothing route-specific belongs here.

source

structure RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) :

Type u

A pooled rank extension of a rank-n representation: a joint law on the pooled structure space and the pooled latent cube, restricting to the representation on the original coordinates and invariant under every sortwise permutation of the pooled carrier — mixed permutations included, which is the load-bearing quantifier. No independence clause of any kind.

law : MeasureTheory.ProbabilityMeasure (S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n)
The joint law on the pooled structure space and the pooled latent cube.
map_restrictOriginal : MeasureTheory.Measure.map (Prod.map S.restrictOriginal (S.restrictOriginalLatents n)) ↑self.law = C.P
Its restriction to the original structure and original-support latents is the representation.
invariant (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) : MeasureTheory.Measure.map (Prod.map (RelStructure.relabel ρ) ⇑(pooledRankLatentRelabel ρ n)) ↑self.law = ↑self.law
Invariance under the full pooled permutation family, acting diagonally on the structure and on the pooled latents.

Instances For

source

noncomputable def RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.pooledTransport {S : RelSignature} {n : ℕ} :

S.RelStructure S.Vinfinite × S.RankLatentSpace n → S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n

The joint transport of the representation onto the pooled carrier: comap poolVertexEquiv on structures, restriction along poolVertexEquiv on latents.

Equations