feat: relatively independent joinings over a common factor (#107)

Graphon.lean

@@ -21,6 +21,8 @@ import Graphon.RelEqualityPattern
 import Graphon.RelKernelEvaluator
 import Graphon.RelKernelSampler
 import Graphon.KernelRandomization
+import Graphon.ForMathlib.RelativeFactorCoupling
+import Graphon.UniformFactorCoupling
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
 import Graphon.RelLowerFactor
@@ -199,6 +201,8 @@ in Lean 4 using Mathlib.
 * `Graphon.RelKernelEvaluator` — R4 evaluator layer (#107): `RelKernelFamily` (the label-free measurable representing kernels `f_{r,π}` on the finite pattern-local latent product), `RelCoord.localLatents` (the coordinate's window into the global latent source), the measurable `evalStructure`, and the **equivariance theorem** `evalStructure_relabel` (relabeling the evaluated structure = precomposing the source with the latent-index action) with the pattern↔image transport square `patternLatentIndexEquivCoord_map` — latent source measure, sampler pushforward, and representation theorem deliberately held for the next layers
 * `Graphon.RelKernelSampler` — R4 sampler layer (#107): the evaluator over an arbitrary carrier (`RelKernelFamily.eval`, definitionally `evalStructure` on `Vinfinite`) with the pullback transport `eval_comap`; the i.i.d. uniform `latentSource` over global subset-latent indices with relabeling invariance (via `LatentIndex.relabelEquiv`); and the **evaluated exchangeable law** `RelKernelFamily.evalLaw` with its **dissociation** `evalLaw_isDissociated` (disjoint vertex windows read disjoint nonempty subset-latent collections, so the i.i.d. source factorizes) — the forward half of the dissociated functional AHK representation; the converse representation theorem is the remaining content of #107
 * `Graphon.KernelRandomization` — R4 converse piece 1 (#107): the small adapter from Mathlib's kernel representation theorem (`Kernel.exists_measurable_map_eq_unitInterval`, Kallenberg Lemma 4.22) to the project's uniform source — `Kernel.exists_measurable_map_eq_uniform01` (a Markov kernel into a standard Borel space is the pushforward of `uniform01` by a jointly measurable map, the `[0,1]`-subtype input adapted through `Set.projIcc`) and the single-measure corollary `Measure.exists_measurable_map_eq_uniform01` — the randomization ("noise outsourcing") input for the converse representation theorem
+* `Graphon.ForMathlib.RelativeFactorCoupling` — **upstream candidate** (signature-free, Mathlib-only imports): the **relatively independent joining over a common factor**, `relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q`, for measurable `q : Ω → Z`, `r : Ξ → Z` with `ν.map r = μ.map q`. Both sides are disintegrated over `Z` and the fibres multiplied independently; the independent product `μ.prod ν` would not identify the factors, and an arbitrary coupling that did could still let each side see more of the other. The engine is `map_condDistrib_id`, **fibre concentration**: pushing `condDistrib id q μ` through `q` is the deterministic identity kernel, i.e. conditioning on `q` pins down `q`. From it: both marginals, the common-factor identity `q ∘ Prod.fst =ᵐ r ∘ Prod.snd` (proved from the two fibre-concentration statements, one per side — equality of the factor *marginals* says nothing about the joint), and `condIndepFun_fst_snd_relativeFactorCoupling`, conditional independence of the two coordinates given `comap (q ∘ Prod.fst)`. The conditioning is deliberately on that variable, defined on the coupling space, rather than on the disintegration variable `∘ₘ` integrates out: only the former is visible to consumers, who see the coupling and not its construction. No σ-algebra equality `σ(q ∘ fst) = σ(snd)` is claimed — the latent may carry strictly more than the factor, as `U` carries more than `1_{U < p}`; what conditional independence excludes is that the surplus says anything further about the first coordinate
+* `Graphon.UniformFactorCoupling` — R4 converse piece 3 (#107): the uniform specialization of the joining above, `exists_relativeFactorCoupling_uniform01`. The only uniform-specific input is `Measure.exists_measurable_map_eq_uniform01` (#140), which supplies the coding map `f : ℝ → Z` matching the two factor laws; everything after is generic. It runs in the direction `Graphon.KernelRandomization` does not — that module manufactures a variable with a prescribed law *out of* a uniform, whereas here a uniform is manufactured *alongside* an already-given variable — and it is reusable at every rank, so it replaces a port of an external de Finetti package with the narrow transfer step the recursion actually needs
 * `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR
 * `Graphon.RelPollingInfrastructure` — R4 (#107): the reusable polling engine, extracted from `RelFixingCondIndep` once the rankwise relative-independence argument became its second consumer. Three public declarations: the tail engine `condExp_ae_eq_condExp_of_comap_eq` (a measure-preserving `T` fixing `f` a.e. and pulling `m₁` back to `m₂ ≤ m₁` forces `μ[f|m₁] =ᵐ μ[f|m₂]`), `InfiniteRelExchangeableLaw.measurePreserving_relabel`, and `InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra`. The `L²` squeeze and the conditional-expectation transport along `comap` stay private — they are the proof of the tail engine, not its interface
 * `Graphon.RelFixingCondIndep` — R4 converse piece 2b (#107): the headline `InfiniteRelExchangeableLaw.condIndep_fixingAlgebra` — for **every** exchangeable law, with no dissociation hypothesis, `CondIndep (fixingAlgebra (A ∩ B)) (fixingAlgebra A) (fixingAlgebra B) (fixingAlgebra_le _) M.law` (Austin arXiv:0801.1698 Lemma 3.11 / Proposition 3.12; Kallenberg Lemma 7.6 as the closest precursor — Lemmas 7.18–7.19 there belong to the later realization recursion). The private machinery: the `L²`-energy squeeze, measure-preserving-map transport of conditional expectation, and the tail-property engine (a.e.-fixing + comap-pullback ⟹ equal conditional expectations); the upgrade of `fixingAlgebra A`-invariance from finitely supported to *arbitrary* sortwise permutations fixing `A`, modulo the law; the poll geometry (deep copies of `B \ A` laid out along a two-sided `ℤ`-orbit — a unilateral block shift is not a bijection — moved by a single residue-wise permutation fixing `A`); the tail **joins** `⨆_{m ≥ n} fixingAlgebra ((A ∩ B) ∪ Q m)`, whose intersection is `fixingAlgebra (A ∩ B)` as a *raw* σ-algebra equality; and the reduction `E[f | fixingAlgebra B] =ᵐ E[f | fixingAlgebra (A ∩ B)]` that the theorem factorizes through. Everything but the headline is `private`

Graphon/ForMathlib/RelativeFactorCoupling.lean

@@ -0,0 +1,211 @@
+/-
+Copyright (c) 2026 Cameron Freer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Freer
+-/
+import Mathlib.Probability.Independence.Conditional
+
+/-!
+# Relatively independent joinings over a common factor
+
+Given two probability spaces carrying a *common factor* — measurable maps `q : Ω → Z` and
+`r : Ξ → Z` with the same pushforward — this file builds the canonical coupling of `μ` and `ν`
+that identifies the two factors and adds nothing else:
+
+`relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q`
+
+Both sides are disintegrated over `Z` and the fibres are then multiplied independently. Nothing
+else would do: the independent product `μ.prod ν` does not satisfy `q X = r Ξ`, and an arbitrary
+coupling with that identity could still let each side see more of the other than the common
+factor does.
+
+## Main results
+
+* `map_condDistrib_id` — **fibre concentration**: the conditional law of a point given its factor
+  value, pushed forward through the factor, is the deterministic identity kernel. This is the
+  whole content of "conditioning on `q` pins down `q`", and everything below rests on it.
+* `map_fst_relativeFactorCoupling`, `map_snd_relativeFactorCoupling` — the two marginals are `μ`
+  and `ν` (the second under the standing hypothesis `ν.map r = μ.map q`).
+* `comp_fst_ae_eq_comp_snd_relativeFactorCoupling` — the **common-factor identity**
+  `q ∘ Prod.fst =ᵐ r ∘ Prod.snd`.
+* `condIndepFun_fst_snd_relativeFactorCoupling` — the two coordinates are conditionally
+  independent **given the common factor read off the first coordinate**.
+
+## Why condition on `q ∘ Prod.fst`
+
+The conditioning σ-algebra is `MeasurableSpace.comap (q ∘ Prod.fst) inferInstance`, generated by a
+genuine random variable on the coupling space, not by an auxiliary `Z`-valued variable that the
+composition `∘ₘ` has integrated out. Only the former is available to downstream consumers, who see
+the coupling and not its construction. The common-factor identity above transfers the statement to
+`r ∘ Prod.snd` whenever that is the more convenient side.
+
+Note that the coupling gives only `σ(q ∘ fst) ⊆ σ(snd)` modulo the law: the second coordinate may
+carry strictly more information than the shared factor, exactly as a uniform `U` carries more than
+`1_{U < p}`. What the conditional independence excludes is that the surplus says anything about
+the first coordinate beyond what the factor already determines.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+namespace ProbabilityTheory
+
+variable {Ω Ξ Z : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω]
+  [MeasurableSpace Ξ] [StandardBorelSpace Ξ] [Nonempty Ξ]
+  [MeasurableSpace Z] [StandardBorelSpace Z] [Nonempty Z]
+
+/-! ### Fibre concentration -/
+
+/-- **Fibre concentration.** The conditional law of a point given the value of a factor map is
+carried by the fibre over that value: pushing `condDistrib id q μ` forward through `q` returns
+the deterministic identity kernel, almost everywhere for the law of the factor. -/
+theorem map_condDistrib_id (μ : Measure Ω) [IsFiniteMeasure μ] {q : Ω → Z} (hq : Measurable q) :
+    (condDistrib id q μ).map q =ᵐ[μ.map q] Kernel.id := by
+  have h₁ : condDistrib (q ∘ (id : Ω → Ω)) q μ =ᵐ[μ.map q] (condDistrib id q μ).map q :=
+    condDistrib_comp q aemeasurable_id hq
+  have h₂ : condDistrib q q μ =ᵐ[μ.map q] Kernel.id := condDistrib_self q
+  have h₃ : condDistrib q q μ =ᵐ[μ.map q] (condDistrib id q μ).map q := by simpa using h₁
+  exact h₃.symm.trans h₂
+
+/-- The fibre over `z` carries all of the conditional law given `z`. -/
+theorem condDistrib_id_apply_fibre (μ : Measure Ω) [IsFiniteMeasure μ] {q : Ω → Z}
+    (hq : Measurable q) :
+    ∀ᵐ z ∂(μ.map q), (condDistrib id q μ) z (q ⁻¹' {z}) = 1 := by
+  filter_upwards [map_condDistrib_id μ hq] with z hz
+  rw [← Measure.map_apply hq (measurableSet_singleton z), ← Kernel.map_apply _ hq, hz,
+    Kernel.id_apply]
+  simp
+
+/-- Pointwise form of fibre concentration: conditionally on the factor value `z`, the factor is
+almost surely equal to `z`. -/
+theorem ae_ae_eq_condDistrib_id (μ : Measure Ω) [IsFiniteMeasure μ] {q : Ω → Z}
+    (hq : Measurable q) :
+    ∀ᵐ z ∂(μ.map q), ∀ᵐ x ∂(condDistrib id q μ) z, q x = z := by
+  filter_upwards [condDistrib_id_apply_fibre μ hq] with z hz
+  rw [ae_iff, show {x | ¬ q x = z} = (q ⁻¹' {z})ᶜ from by ext x; simp]
+  exact (prob_compl_eq_zero_iff (hq (measurableSet_singleton z))).mpr hz
+
+/-! ### The coupling -/
+
+/-- **The relatively independent joining of `μ` and `ν` over their common `Z`-factor.** Both sides
+are disintegrated over `Z` — `μ` along `q`, `ν` along `r` — and the fibres are then multiplied
+independently. -/
+noncomputable def relativeFactorCoupling (μ : Measure Ω) (ν : Measure Ξ) [IsFiniteMeasure μ]
+    [IsFiniteMeasure ν] (q : Ω → Z) (r : Ξ → Z) : Measure (Ω × Ξ) :=
+  ((condDistrib id q μ) ×ₖ (condDistrib id r ν)) ∘ₘ (μ.map q)
+
+instance instIsFiniteMeasureRelativeFactorCoupling (μ : Measure Ω) (ν : Measure Ξ)
+    [IsFiniteMeasure μ] [IsFiniteMeasure ν] (q : Ω → Z) (r : Ξ → Z) :
+    IsFiniteMeasure (relativeFactorCoupling μ ν q r) := by
+  haveI : IsFiniteMeasure (μ.map q) := Measure.isFiniteMeasure_map μ q
+  rw [relativeFactorCoupling]
+  infer_instance
+
+variable {μ : Measure Ω} {ν : Measure Ξ} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
+  {q : Ω → Z} {r : Ξ → Z}
+
+omit [StandardBorelSpace Z] [Nonempty Z] in
+/-- The coupling is a probability measure. Measurability of `q` is genuinely needed: without it
+`μ.map q` is the zero measure. -/
+theorem isProbabilityMeasure_relativeFactorCoupling (hq : Measurable q) :
+    IsProbabilityMeasure (relativeFactorCoupling μ ν q r) := by
+  haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable
+  rw [relativeFactorCoupling]
+  infer_instance
+
+omit [StandardBorelSpace Z] [Nonempty Z] in
+/-- The first marginal is `μ`. -/
+theorem map_fst_relativeFactorCoupling (hq : Measurable q) :
+    (relativeFactorCoupling μ ν q r).map Prod.fst = μ := by
+  rw [relativeFactorCoupling, Measure.map_comp _ _ measurable_fst, ← Kernel.fst_eq, Kernel.fst_prod]
+  simpa using condDistrib_comp_map (X := q) hq.aemeasurable (aemeasurable_id (μ := μ))
+
+omit [StandardBorelSpace Z] [Nonempty Z] in
+/-- The second marginal is `ν`, under the standing hypothesis that the two factors have the same
+law. -/
+theorem map_snd_relativeFactorCoupling (hr : Measurable r) (hqr : ν.map r = μ.map q) :
+    (relativeFactorCoupling μ ν q r).map Prod.snd = ν := by
+  rw [relativeFactorCoupling, Measure.map_comp _ _ measurable_snd, ← Kernel.snd_eq,
+    Kernel.snd_prod, ← hqr]
+  simpa using condDistrib_comp_map (μ := ν) (X := r) hr.aemeasurable (aemeasurable_id (μ := ν))
+
+/-- **The common-factor identity**: the two coordinates agree on the shared factor. Proved from
+the two fibre-concentration statements, one on each side of the joining — equality of the two
+factor *marginals* would not suffice, since it says nothing about the joint law. -/
+theorem comp_fst_ae_eq_comp_snd_relativeFactorCoupling (hq : Measurable q) (hr : Measurable r)
+    (hqr : ν.map r = μ.map q) :
+    q ∘ Prod.fst =ᵐ[relativeFactorCoupling μ ν q r] r ∘ Prod.snd := by
+  haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable
+  have hmeas : MeasurableSet {p : Ω × Ξ | (q ∘ Prod.fst) p = (r ∘ Prod.snd) p} :=
+    measurableSet_eq_fun (hq.comp measurable_fst) (hr.comp measurable_snd)
+  have hν : ∀ᵐ z ∂(μ.map q), ∀ᵐ y ∂(condDistrib id r ν) z, r y = z := by
+    rw [← hqr]; exact ae_ae_eq_condDistrib_id ν hr
+  rw [Filter.EventuallyEq, relativeFactorCoupling, Measure.ae_comp_iff hmeas]
+  filter_upwards [ae_ae_eq_condDistrib_id μ hq, hν] with z hz hz'
+  rw [Kernel.prod_apply]
+  have h1 : ∀ᵐ p ∂(((condDistrib id q μ) z).prod ((condDistrib id r ν) z)), q p.1 = z :=
+    Measure.quasiMeasurePreserving_fst.ae hz
+  have h2 : ∀ᵐ p ∂(((condDistrib id q μ) z).prod ((condDistrib id r ν) z)), r p.2 = z :=
+    Measure.quasiMeasurePreserving_snd.ae hz'
+  filter_upwards [h1, h2] with p hp1 hp2
+  simp only [Function.comp_apply, hp1, hp2]
+
+/-- The joint law of the common factor and the two coordinates: the factor is a.s. the
+disintegration variable, so reading it off the first coordinate reconstitutes the outer
+integration. This is the structural identity behind the conditional independence below. -/
+theorem map_factorProd_relativeFactorCoupling (hq : Measurable q) :
+    (relativeFactorCoupling μ ν q r).map (fun p => (q p.1, p.1, p.2))
+      = (Kernel.id ×ₖ ((condDistrib id q μ) ×ₖ (condDistrib id r ν))) ∘ₘ (μ.map q) := by
+  haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable
+  have hw : Measurable (fun p : Ω × Ξ => (q p.1, p.1, p.2)) :=
+    (hq.comp measurable_fst).prodMk measurable_id
+  rw [relativeFactorCoupling, Measure.map_comp _ _ hw]
+  refine Measure.comp_congr ?_
+  filter_upwards [ae_ae_eq_condDistrib_id μ hq] with z hz
+  rw [Kernel.map_apply _ hw, Kernel.prod_apply, Kernel.prod_apply, Kernel.id_apply,
+    Measure.dirac_prod, Kernel.prod_apply]
+  refine Measure.map_congr ?_
+  have h1 : ∀ᵐ p ∂(((condDistrib id q μ) z).prod ((condDistrib id r ν) z)), q p.1 = z :=
+    Measure.quasiMeasurePreserving_fst.ae hz
+  filter_upwards [h1] with p hp
+  simp [hp]
+
+/-- **The two coordinates are conditionally independent given the common factor.** The
+conditioning σ-algebra is the one generated by `q ∘ Prod.fst`, a random variable on the coupling
+space itself rather than the integrated-out disintegration variable. -/
+theorem condIndepFun_fst_snd_relativeFactorCoupling (hq : Measurable q) (hr : Measurable r)
+    (hqr : ν.map r = μ.map q) :
+    CondIndepFun (MeasurableSpace.comap (q ∘ Prod.fst) inferInstance)
+      (hq.comp measurable_fst).comap_le Prod.fst Prod.snd (relativeFactorCoupling μ ν q r) := by
+  haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable
+  set P := relativeFactorCoupling μ ν q r with hP
+  -- the law of the common factor on the coupling space
+  have hmapk : P.map (q ∘ Prod.fst) = μ.map q := by
+    rw [hP, ← Measure.map_map hq measurable_fst, map_fst_relativeFactorCoupling hq]
+  -- the two conditional distributions are the two disintegration kernels
+  have hcd1 : condDistrib Prod.fst (q ∘ Prod.fst) P =ᵐ[μ.map q] condDistrib id q μ := by
+    rw [← hmapk, condDistrib_ae_eq_iff_measure_eq_compProd _ measurable_fst.aemeasurable, hmapk,
+      compProd_map_condDistrib (aemeasurable_id (μ := μ))]
+    rw [show (fun p : Ω × Ξ => ((q ∘ Prod.fst) p, p.1)) = (fun x : Ω => (q x, id x)) ∘ Prod.fst from
+      rfl, ← Measure.map_map (by fun_prop) measurable_fst, hP,
+      map_fst_relativeFactorCoupling hq]
+  have hcd2 : condDistrib Prod.snd (q ∘ Prod.fst) P =ᵐ[μ.map q] condDistrib id r ν := by
+    rw [← hmapk, condDistrib_ae_eq_iff_measure_eq_compProd _ measurable_snd.aemeasurable, hmapk,
+      ← hqr, compProd_map_condDistrib (aemeasurable_id (μ := ν))]
+    have hswap : P.map (fun p : Ω × Ξ => ((q ∘ Prod.fst) p, p.2))
+        = P.map (fun p : Ω × Ξ => (r p.2, id p.2)) := by
+      refine Measure.map_congr ?_
+      filter_upwards [comp_fst_ae_eq_comp_snd_relativeFactorCoupling hq hr hqr] with p hp
+      rw [show ((q ∘ Prod.fst) p, p.2) = ((r ∘ Prod.snd) p, p.2) from by rw [hp]]
+      rfl
+    rw [hswap, show (fun p : Ω × Ξ => (r p.2, id p.2)) = (fun y : Ξ => (r y, id y)) ∘ Prod.snd from
+      rfl, ← Measure.map_map (by fun_prop) measurable_snd, hP,
+      map_snd_relativeFactorCoupling hr hqr]
+  rw [condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib measurable_fst measurable_snd
+    (hq.comp measurable_fst), hmapk]
+  simp only [Function.comp_apply]
+  rw [map_factorProd_relativeFactorCoupling hq]
+  refine (Measure.comp_congr ?_).symm
+  filter_upwards [hcd1, hcd2] with z h1 h2
+  rw [Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply, h1, h2]
+
+end ProbabilityTheory