The rank-one coupling on the latent space (R4 converse piece 3, #107)

The #161 coupling relativeFactorCoupling M.law uniform01 (lowerFactorMap 1) f lives on RelStructure × ℝ. The RankRepresentation interface asks for a coupling with the rank-one latent space RankLatentSpace S 1 — the one-coordinate cube the recursion indexes by supports — as its second factor. This module transports the coupling (rankOneLatentCoupling) and all its clauses through rankLatentOneEquiv : RankLatentSpace S 1 ≃ᵐ ℝ, applied on the second coordinate only.

Two clauses deserve comment.

• Joint relabeling invariance comes out in the RankRepresentation shape: the relabeling acts on both coordinates at once. At rank one rankLatentRelabel σ 1 is the identity on points (rankLatentRelabel_one_eq), so the latent side of the joint action collapses and #161's structure-side invariance map_prodMap_relabel_rankOneCoupling is exactly what is needed. At higher rank neither simplification is available.
• Conditional independence transports along the reverse direction: the second-coordinate equivalence is measure-preserving from the transported coupling back to the original, the pair transport condIndepFun_comp_measurePreserving moves the clause, MeasurableSpace.comap_comp collapses the conditioning — the equivalence does not touch the first coordinate — and Mathlib's CondIndepFun.comp straightens the codomain.

As in #161, the conditional-independence clause is stated for every measurable reading of the structure, so any unresolved reading follows by composition; and no σ-algebra equality between the latent and the factor is claimed — the latent may carry strictly more than lowerFactorMap 1 reads, and conditional independence is exactly the statement that the surplus says nothing further about the structure.

noncomputable def RelSignature.rankOneLatentEquiv (S : RelSignature) : S.RelStructure S.Vinfinite × ℝ ≃ᵐ S.RelStructure S.Vinfinite × S.RankLatentSpace 1

The second-coordinate transport: identity on the structure, rankLatentOneEquiv.symm on the latent. Mentions no basis and no law, so it lives at the signature level.

Equations

• S.rankOneLatentEquiv = (MeasurableEquiv.refl (S.RelStructure S.Vinfinite)).prodCongr RelSignature.rankLatentOneEquiv.symm

theorem RelSignature.rankOneLatentEquiv_coe (S : RelSignature) : ⇑S.rankOneLatentEquiv = Prod.map id ⇑rankLatentOneEquiv.symm

theorem RelSignature.rankOneLatentEquiv_symm_coe (S : RelSignature) : ⇑S.rankOneLatentEquiv.symm = Prod.map id ⇑rankLatentOneEquiv

noncomputable def RelSignature.CoherentBasis.rankOneLatentCoupling {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Countable S.Srt] [Countable S.Rel] (f : ℝ → B.LowerFactorSpace 1) : MeasureTheory.Measure (S.RelStructure S.Vinfinite × S.RankLatentSpace 1)

The rank-one coupling, on the latent space: the #161 coupling with its latent coordinate transported into the rank-one latent cube.

Equations

• B.rankOneLatentCoupling f = MeasureTheory.Measure.map (⇑S.rankOneLatentEquiv) (ProbabilityTheory.relativeFactorCoupling (↑M.law) MeasureTheory.uniform01 (B.lowerFactorMap 1) f)

instance RelSignature.CoherentBasis.instIsFiniteMeasureProdRelStructureVinfiniteRankLatentSpaceOfNatNatRankOneLatentCoupling {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Countable S.Srt] [Countable S.Rel] (f : ℝ → B.LowerFactorSpace 1) : MeasureTheory.IsFiniteMeasure (B.rankOneLatentCoupling f)

theorem RelSignature.CoherentBasis.exists_rankOneLatentCoupling {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Countable S.Srt] [Countable S.Rel] : ∃ (f : ℝ → B.LowerFactorSpace 1) (g : S.RankLatentSpace 1 → B.LowerFactorSpace 1), Measurable g ∧ MeasureTheory.IsProbabilityMeasure (B.rankOneLatentCoupling f) ∧ MeasureTheory.Measure.map Prod.fst (B.rankOneLatentCoupling f) = ↑M.law ∧ MeasureTheory.Measure.map Prod.snd (B.rankOneLatentCoupling f) = S.rankLatentSource 1 ∧ (∀ (σ : ↥S.FinSuppPerm), MeasureTheory.Measure.map (Prod.map (RelStructure.relabel ↑σ) ⇑(rankLatentRelabel σ 1)) (B.rankOneLatentCoupling f) = B.rankOneLatentCoupling f) ∧ B.lowerFactorMap 1 ∘ Prod.fst =ᵐ[B.rankOneLatentCoupling f] g ∘ Prod.snd ∧ ∀ {Y : Type u_1} [inst : MeasurableSpace Y] {h : S.RelStructure S.Vinfinite → Y}, Measurable h → ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (B.lowerFactorMap 1 ∘ Prod.fst) inferInstance) ⋯ (h ∘ Prod.fst) Prod.snd (B.rankOneLatentCoupling f)

The transported clauses. There are a coding f and a measurable latent read g for which the rank-one latent coupling is a probability measure with the law and the latent source as marginals, is invariant under the joint relabeling action, resolves the rank-one factor through g, and makes the latent conditionally independent — given the rank-one factor — of every measurable reading of the structure.