The step kernel of a coherent factor (R4 converse piece 3, #107)

One kernel per finite tagged vertex set A: the conditional distribution of the exact-anchor layer at A given the whole proper-subset boundary.

stepKernel A : Kernel (BoundarySpace A) (ExactSpace A) is condDistrib of the exact-anchor map given the boundary map. The standard Borel structure of ExactSpace A — countable index, Boolean values — is exactly the hypothesis condDistrib needs, which is what the factor-space packaging was for.

Everything here is valid for an arbitrary exchangeable law. In particular the A = ∅ base case is deliberately not treated: its determinism uses dissociation, whereas stepKernel should stay available without it. That base case belongs to the later realization/recursion layer.

Central identities

• compProd_stepKernel — the disintegration boundaryLaw A ⊗ₘ stepKernel A = M.law.map fun ω => (boundaryMap A ω, exactMap A ω);
• stepKernel_comp_boundaryLaw — marginal recovery stepKernel A ∘ₘ boundaryLaw A = exactLaw A;
• factorLaw_map_prodEquiv — the same statement read through the product decomposition.

The step kernel

noncomputable def RelSignature.CoherentBasis.stepKernel {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ProbabilityTheory.Kernel (B.BoundarySpace A) (B.ExactSpace A)

The step kernel at A: the conditional distribution of the exact-anchor layer given the boundary layer. One kernel per finite A, conditioned on the whole proper-subset boundary at once — not one per pair C ⊆ A, and not a chain.

Equations

• B.stepKernel A = ProbabilityTheory.condDistrib (B.exactMap A) (B.boundaryMap A) ↑M.law

instance RelSignature.CoherentBasis.instIsMarkovKernelBoundarySpaceExactSpaceStepKernel {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ProbabilityTheory.IsMarkovKernel (B.stepKernel A)

theorem RelSignature.CoherentBasis.compProd_stepKernel {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : (B.boundaryLaw A).compProd (B.stepKernel A) = MeasureTheory.Measure.map (fun (ω : S.RelStructure S.Vinfinite) => (B.boundaryMap A ω, B.exactMap A ω)) ↑M.law

Disintegration: the joint law of the boundary and exact-anchor layers is the boundary law composed with the step kernel.

theorem RelSignature.CoherentBasis.stepKernel_comp_boundaryLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : (B.boundaryLaw A).bind ⇑(B.stepKernel A) = B.exactLaw A

Marginal recovery: composing the step kernel with the boundary law returns the exact law.

theorem RelSignature.CoherentBasis.factorSpaceProdEquiv_factorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : (fun (ω : S.RelStructure S.Vinfinite) => (B.factorSpaceProdEquiv A) (B.factorMap A ω)) = fun (ω : S.RelStructure S.Vinfinite) => (B.boundaryMap A ω, B.exactMap A ω)

The factor map is the pair of its two layers, by definition of the layer maps.

theorem RelSignature.CoherentBasis.factorLaw_map_prodEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure.map (⇑(B.factorSpaceProdEquiv A)) (B.factorLaw A) = (B.boundaryLaw A).compProd (B.stepKernel A)

The disintegration read through the product decomposition: pushing the factor law along factorSpaceProdEquiv gives the boundary law composed with the step kernel.

Relabeling transport

theorem RelSignature.CoherentBasis.map_prodMap_compProd_stepKernel {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure.map (Prod.map ⇑(B.boundarySpaceEquiv σ A) ⇑(B.exactSpaceEquiv σ A)) ((B.boundaryLaw (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)).compProd (B.stepKernel (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A))) = (B.boundaryLaw A).compProd (B.stepKernel A)

Exact transport of the joint law: pushing the boundary-and-exact joint law at the image vertex set along the two layer equivalences returns the joint law at A.

This is an equality of measures, not an a.e. statement: it follows from equivariance of the splitting (prodMap_comp_factorSpaceProdEquiv, definitional) together with relabeling invariance of the factor law, which is where exchangeability enters.

theorem RelSignature.CoherentBasis.stepKernel_map_ae_eq_comap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ⇑((B.stepKernel (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)).map ⇑(B.exactSpaceEquiv σ A)) =ᵐ[B.boundaryLaw (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)] ⇑((B.stepKernel A).comap ⇑(B.boundarySpaceEquiv σ A) ⋯)

Kernel transport under relabeling, stated a.e. under the source boundary law.

A conditional distribution is unique only almost everywhere, so this is an a.e. equality of kernels and no strict coherence is claimed. The orientation is the source one the recursion needs: the step kernel at the image vertex set, with its target relabeled, agrees with the step kernel at A pulled back along the boundary equivalence.

Proof: both composition-products agree after pushing forward by MeasurableEquiv.prodCongr (boundarySpaceEquiv σ A) (.refl _) — the left side by Measure.compProd_map and the exact joint transport, the right side by the change-of-variables helper and the boundary-law transport — and a measurable equivalence has injective pushforward, so Kernel.compProd_eq_iff concludes.