feat: pooled-latent gate stage 3 — joint restriction, law identity, and the four consequences (#195)

Graphon/ForMathlib/CondIndepSup.lean

@@ -6,9 +6,9 @@ Authors: Cameron Freer
 import Mathlib.Probability.Independence.Conditional
 
 /-!
-# Two closure properties of conditional independence
+# Three closure properties of conditional independence
 
-Both are glue Mathlib does not currently provide.
+All three are glue Mathlib does not currently provide.
 
 * **Joining the conditioning algebra to one side is free**: from `m₁ ⊥⊥ m₂ ∣ m'` conclude
   `m₁ ⊥⊥ (m' ⊔ m₂) ∣ m'`. Whatever the conditioning algebra already knows cannot carry new
@@ -24,6 +24,12 @@ Both are glue Mathlib does not currently provide.
 
 Neither statement mentions this repository's signatures. The `[StandardBorelSpace Ω]` hypotheses
 come with Mathlib's definition of `CondIndep`/`CondIndepFun` through `condExpKernel`.
+
+* **The conditioning σ-algebra may be replaced by an equal one** (`CondIndepFun.congr_cond`): the
+  dependent `≤` proof moves by proof irrelevance once the σ-algebra equality is substituted. Needed
+  wherever a conditioning map is reindexed — the rank-one coupling and screening arguments and the
+  pooled screening transport all consume it.
+
 -/
 
 open MeasureTheory
@@ -106,4 +112,16 @@ theorem CondIndepFun.congr {β β' : Type*} {mβ : MeasurableSpace β} {mβ' : M
     _ =ᵐ[μ] fun ω => (μ⟦f' ⁻¹' s | m'⟧) ω * (μ⟦g' ⁻¹' t | m'⟧) ω :=
         ((hsets h1).symm.mul (hsets h2).symm)
 
+/-- **The conditioning σ-algebra may be replaced by an equal one.** The dependent `≤` proof is
+handled by proof irrelevance once the σ-algebra equality is substituted. Shared glue: the rank-one
+coupling and screening arguments both need it, and so does any transport of a conditional
+independence statement whose conditioning map has been reindexed. -/
+theorem CondIndepFun.congr_cond {Ω β γ : Type*} [mΩ : MeasurableSpace Ω]
+    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
+    [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
+    {m₁ m₂ : MeasurableSpace Ω} {h1 : m₁ ≤ mΩ} (h : CondIndepFun m₁ h1 f g μ)
+    (h12 : m₁ = m₂) (h2 : m₂ ≤ mΩ) : CondIndepFun m₂ h2 f g μ := by
+  subst h12
+  exact h
+
 end ProbabilityTheory

Graphon/PermutationExtension.lean

@@ -43,3 +43,25 @@ theorem exists_perm_extend {k : ℕ} (g : Fin k ↪ ℕ) :
   show ((Equiv.ofInjective g g.injective)
     ((Equiv.ofInjective _ Fin.val_injective).symm ⟨(↑a : ℕ), ⟨a, rfl⟩⟩) : ℕ) = g a
   rw [h1]; rfl
+
+/-- **Every finite partial injection of `ℕ` extends to a permutation**: the domain and its image
+are finite, so their complements are countably infinite and hence equivalent, and
+`Equiv.Set.compl` assembles the permutation. Generalizes `exists_perm_extend` from an initial
+segment to an arbitrary finite domain. -/
+theorem exists_perm_extend_of_injOn {A : Finset ℕ} {g : ℕ → ℕ} (hg : Set.InjOn g ↑A) :
+    ∃ σ : Equiv.Perm ℕ, ∀ a ∈ A, σ a = g a := by
+  classical
+  let e₀ : (↑A : Set ℕ) ≃ (g '' ↑A : Set ℕ) := Equiv.Set.imageOfInjOn g (↑A : Set ℕ) hg
+  have hsc : ((↑A : Set ℕ)ᶜ).Infinite := (A.finite_toSet).infinite_compl
+  have htc : ((g '' ↑A : Set ℕ)ᶜ).Infinite :=
+    ((A.finite_toSet).image g).infinite_compl
+  haveI := hsc.to_subtype
+  haveI := htc.to_subtype
+  haveI : Denumerable ((↑A : Set ℕ)ᶜ : Set ℕ) := Denumerable.ofEncodableOfInfinite _
+  haveI : Denumerable ((g '' ↑A : Set ℕ)ᶜ : Set ℕ) := Denumerable.ofEncodableOfInfinite _
+  obtain ⟨σ, hσ⟩ := (Equiv.Set.compl e₀).symm
+    ((Denumerable.eqv _).trans (Denumerable.eqv _).symm)
+  refine ⟨σ, fun a ha => ?_⟩
+  have h := hσ ⟨a, ha⟩
+  rw [h]
+  rfl

Graphon/RelLatentGeometry.lean

@@ -238,6 +238,76 @@ theorem latentRestrictOver_toEmbedding (ρ : ∀ s, Equiv.Perm (V s)) (n : ℕ)
   refine Finset.ext fun v => ?_
   simp [Finset.mem_image]
 
+open scoped Classical in
+/-- **Support-wise agreement**: if a permutation of the target carrier carries one embedding to
+another on every vertex of a support, the two induced index maps agree there. Stated with
+abstract carriers, so instantiating never manipulates `Finset.image` under a derived
+`DecidableEq`. -/
+theorem latentIndexEmbed_eq_of_agree {e f : ∀ s, V s ↪ W s} {ρ : ∀ s, Equiv.Perm (W s)} {n : ℕ}
+    {A : LatentIndexOver S V n} (h : ∀ v ∈ A.1, ρ v.1 (e v.1 v.2) = f v.1 v.2) :
+    latentIndexEmbed f n A = latentIndexPerm ρ n (latentIndexEmbed e n A) := by
+  refine Subtype.ext ?_
+  rw [latentIndexEmbed_coe, latentIndexPerm_apply_coe, latentIndexEmbed_coe, Finset.image_image]
+  refine Finset.image_congr fun v hv => ?_
+  obtain ⟨s, x⟩ := v
+  show (⟨s, f s x⟩ : Σ s : S.Srt, W s) = ⟨s, ρ s (e s x)⟩
+  rw [h ⟨s, x⟩ hv]
+
+open scoped Classical in
+/-- Restriction along the identity embedding is the identity. -/
+theorem latentIndexEmbed_refl (n : ℕ) (A : LatentIndexOver S V n) :
+    latentIndexEmbed (fun s => Function.Embedding.refl (V s)) n A = A := by
+  refine Subtype.ext ?_
+  rw [latentIndexEmbed_coe]
+  refine (Finset.image_congr fun v _ => ?_).trans A.1.image_id
+  obtain ⟨s, x⟩ := v
+  rfl
+
+/-- **The index bijection induced by a carrier equivalence.** -/
+noncomputable def latentIndexCongr (e : ∀ s, V s ≃ W s) (n : ℕ) :
+    LatentIndexOver S V n ≃ LatentIndexOver S W n where
+  toFun := latentIndexEmbed (fun s => (e s).toEmbedding) n
+  invFun := latentIndexEmbed (fun s => (e s).symm.toEmbedding) n
+  left_inv A := by
+    rw [latentIndexEmbed_comp]
+    refine Eq.trans ?_ (latentIndexEmbed_refl n A)
+    congr 1
+    funext s
+    exact Function.Embedding.ext fun x => (e s).symm_apply_apply x
+  right_inv A := by
+    rw [latentIndexEmbed_comp]
+    refine Eq.trans ?_ (latentIndexEmbed_refl n A)
+    congr 1
+    funext s
+    exact Function.Embedding.ext fun x => (e s).apply_symm_apply x
+
+/-- **Transport of the latent cube along a carrier equivalence**, as a measurable equivalence.
+Its forward map is restriction along the equivalence, so the organizing restriction theorem can be
+cancelled rather than merely stated. -/
+noncomputable def latentCongrOver (e : ∀ s, V s ≃ W s) (n : ℕ) :
+    LatentSpaceOver S W n ≃ᵐ LatentSpaceOver S V n where
+  toEquiv := Equiv.arrowCongr (latentIndexCongr e n).symm (Equiv.refl ℝ)
+  measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+  measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+@[simp] theorem latentCongrOver_apply (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (ω : LatentSpaceOver S W n) :
+    latentCongrOver e n ω = latentRestrictOver (fun s => (e s).toEmbedding) n ω := rfl
+
+@[simp] theorem latentCongrOver_symm_apply (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (ω : LatentSpaceOver S V n) :
+    (latentCongrOver e n).symm ω =
+      latentRestrictOver (fun s => (e s).symm.toEmbedding) n ω := rfl
+
+/-- **Exact source transport along a carrier equivalence.** The same infinite-product
+coordinate-equivalence argument as source invariance, with the index bijection now coming from an
+equivalence of carriers rather than a permutation of one. -/
+theorem latentSourceOver_map_latentCongrOver [Countable S.Srt] [∀ s, Countable (V s)]
+    [∀ s, Countable (W s)] (e : ∀ s, V s ≃ W s) (n : ℕ) :
+    (latentSourceOver S W n).map (latentCongrOver e n) = latentSourceOver S V n := by
+  rw [latentSourceOver, latentSourceOver, iidUniformSource, iidUniformSource]
+  exact Measure.infinitePi_map_comp_equiv _ (latentIndexCongr e n)
+
 /-- **The conjugation square for a carrier equivalence** — the latent-side mirror of
 `RelStructure.congrCarrier_relabel`. Transporting along `e` intertwines a permutation of the
 source carrier with its conjugate on the target. Proved carrier-generically, so instantiating at