refactor: delete dead local Kernel.IndepFun.comp duplicate (−41 lines)#22
Merged
Merged
Conversation
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
This was referenced May 18, 2026
Merged
cameronfreer
added a commit
that referenced
this pull request
May 18, 2026
…ib (#31) The local `MartingaleHelpers.comap_comp_le` lemma had one real caller (`RevFiltration.lean:109`) and was a thin wrapper around the mathlib chain `MeasurableSpace.comap_comp` (equality) + `comap_mono` + the target function's `.comap_le`. Inline at the call site: rw [← MeasurableSpace.comap_comp] exact MeasurableSpace.comap_mono measurable_shiftSeq.comap_le The other two references to the lemma — `open ...MartingaleHelpers (comap_comp_le)` in `ViaKoopman/InfraCore.lean:103` and `ViaKoopman/KernelBridge.lean:31` — were vestigial after PR #22 (which deleted the local `Kernel.IndepFun.comp` that had used `comap_comp_le` internally). Dropped. - DeFinetti/MartingaleHelpers.lean: delete the lemma + its `section ComapTools` wrapper (-19 lines). - DeFinetti/ViaMartingale/RevFiltration.lean: inline the call (-0 lines net; 2 lines for 1). - DeFinetti/ViaKoopman/{InfraCore,KernelBridge}.lean: drop the vestigial `open` statements (-1 line each). Net -21 lines across 4 files. Build clean (3527 jobs), axioms standard, 0 sorries.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
KernelBridge.leandefined a localKernel.IndepFun.complemma that duplicates mathlib'sProbabilityTheory.Kernel.IndepFun.comp(specialized to ℝ-valued composition targets). It has zero callers in the codebase. Delete it.Net diff: 1 file, +0 / −41 (−41 lines, pure deletion).
Why this is a deletion, not a wrapper
The PR #16 autoGolf draft proposed making the local lemma a thin wrapper around
ProbabilityTheory.Kernel.IndepFun.comp. But the wrapper has no callers: I grep'd for allKernel.IndepFun.compusages and all.compdot-notation calls onKernel.IndepFun/IndepFuninstances:Probability/CondIndep/Indicator.lean:135, 144, 150, 179— these use_indep.compon plainIndepFun(measure-based), so dot notation resolves to mathlib'sProbabilityTheory.IndepFun.comp(different lemma, different namespace).Probability/CondIndep/Basic.lean:161, 168— same.KernelBridge.lean:17— module docstring bullet (advertising the lemma).DeFinetti/ProofPlan.lean:50— historical planning note ("already proved").No code actually calls
Kernel.IndepFun.comp(the kernel-based one). Replacing the body with a wrapper would leave dead code; deleting is the right move.What changed
Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean:Kernel.IndepFun.comp(lines 181–219).The
DeFinetti/ProofPlan.lean:50historical note is left alone — it's a session-archaeology document, not user-facing.If a future
Kernel.IndepFunterm needs.comp, dot notation will resolve to mathlib'sProbabilityTheory.Kernel.IndepFun.compvia the existing imports, with a strictly more general signature (target type need not be ℝ).Verification
lake buildExchangeability+ForMathlib)Notes