From 83b1363d2e7de37bd5d282c822dd3c40c2943221 Mon Sep 17 00:00:00 2001
From: Cameron Freer <freer@mit.edu>
Date: Mon, 18 May 2026 02:01:17 +0000
Subject: [PATCH] refactor: delete dead local Kernel.IndepFun.comp duplicate
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

KernelBridge.lean defines a local `Kernel.IndepFun.comp` lemma that
duplicates mathlib's `ProbabilityTheory.Kernel.IndepFun.comp` (specialized
to ℝ-valued composition targets). It has zero callers in the codebase:
the `_indep.comp` calls in `Probability/CondIndep/Indicator.lean` and
`Probability/CondIndep/Basic.lean` are on plain `IndepFun` (measure-based),
which resolves to mathlib's `ProbabilityTheory.IndepFun.comp` — a different
lemma in a different namespace.

This delete is stronger than PR #16's autoGolf suggestion (which kept the
lemma as a thin wrapper). Since there is nothing to wrap to, removing it
outright is cleaner.

- Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean:
  - delete the 30-line proof + 10-line docstring (lines 181-219)
  - update the module docstring "Main results" bullet list to match
---
 .../DeFinetti/ViaKoopman/KernelBridge.lean    | 41 -------------------
 1 file changed, 41 deletions(-)

diff --git a/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean b/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
index 4e39becf..2374bf15 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
@@ -14,7 +14,6 @@ This file contains bridge lemmas connecting kernel-level and measure-level indep
 ## Main results
 
 - `Kernel.IndepFun.ae_measure_indepFun`: Kernel independence implies measure-level integral factorization
-- `Kernel.IndepFun.comp`: Independence is preserved under composition with measurable functions
 - `metProjection_eq_condExpL2_shiftInvariant`: MET projection equals conditional expectation
 
 **Split from**: KernelIndependence.lean (lines 1-280)
@@ -178,46 +177,6 @@ lemma Kernel.IndepFun.ae_measure_indepFun
   exact h_indep.integral_fun_mul_eq_mul_integral
     hX.aestronglyMeasurable hY.aestronglyMeasurable
 
-/-- **Composition lemma**: Independence is preserved under composition with measurable functions.
-
-If X and Y are kernel-independent, then f ∘ X and g ∘ Y are also kernel-independent
-for any measurable functions f and g.
-
-**Proof strategy**:
-- Kernel.IndepFun X Y κ μ means Kernel.Indep (comap X) (comap Y) κ μ
-- For measurable f, comap (f ∘ X) ⊆ comap X (preimages under f∘X are preimages under X)
-- Independence of larger σ-algebras implies independence of sub-σ-algebras
--/
-lemma Kernel.IndepFun.comp
-    {α Ω β γ : Type*} [MeasurableSpace α] [MeasurableSpace Ω]
-    [MeasurableSpace β] [MeasurableSpace γ]
-    {κ : Kernel α Ω} {μ : Measure α}
-    {X : Ω → β} {Y : Ω → γ}
-    (hXY : Kernel.IndepFun X Y κ μ)
-    {f : β → ℝ} {g : γ → ℝ}
-    (hf : Measurable f) (hg : Measurable g) :
-    Kernel.IndepFun (f ∘ X) (g ∘ Y) κ μ := by
-  -- The key insight: Kernel.IndepFun is defined as independence of the comap σ-algebras
-  -- For sets s, t in the target σ-algebras, we need to show:
-  -- ∀ s ∈ σ(f∘X), ∀ t ∈ σ(g∘Y), ∀ᵐ a, κ a (s ∩ t) = κ a s * κ a t
-
-  intro s t hs ht
-  -- s is measurable w.r.t. comap (f ∘ X), so s = (f ∘ X)⁻¹(S) for some measurable S ⊆ ℝ
-  -- This means s = X⁻¹(f⁻¹(S)), so s is in comap X
-  -- Similarly t is in comap Y
-
-  -- We need to show s ∈ comap X and t ∈ comap Y
-  -- Key fact: if s is measurable w.r.t. comap (f ∘ X), then s is measurable w.r.t. comap X
-  -- because comap (f ∘ X) ≤ comap X
-
-  have hs' : MeasurableSet[MeasurableSpace.comap X inferInstance] s :=
-    comap_comp_le X f hf s hs
-
-  have ht' : MeasurableSet[MeasurableSpace.comap Y inferInstance] t :=
-    comap_comp_le Y g hg t ht
-
-  exact hXY s t hs' ht'
-
 /-- **Bridge lemma**: The Mean Ergodic Theorem projection equals conditional expectation
 onto the shift-invariant σ-algebra.