Skip to content

refactor: delete comap_comp_le wrapper, route call site through mathlib (−21 lines) #31

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
cameronfreer merged 1 commit into from
May 18, 2026
Merged

refactor: delete comap_comp_le wrapper, route call site through mathlib (−21 lines) #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 0 additions & 19 deletions Exchangeability/DeFinetti/MartingaleHelpers.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,25 +50,6 @@ export PathSpace (tailCylinder tailCylinder_measurable cylinder finCylinder

open MeasureTheory

section ComapTools

/-- If `g` is measurable, then `comap (g ∘ f) ≤ comap f`. -/
@[nolint unusedArguments]
lemma comap_comp_le
{X Y Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
(f : X → Y) (g : Y → Z) (hg : Measurable g) :
MeasurableSpace.comap (g ∘ f) (inferInstance : MeasurableSpace Z)
≤ MeasurableSpace.comap f (inferInstance : MeasurableSpace Y) := by
intro s hs
-- s is a set in the comap (g ∘ f) algebra, so s = (g ∘ f) ⁻¹' t for some t
obtain ⟨t, ht, rfl⟩ := hs
-- Show (g ∘ f) ⁻¹' t is in comap f
refine ⟨g ⁻¹' t, hg ht, ?_⟩
ext x
simp [Set.mem_preimage, Function.comp_apply]

end ComapTools

section SequenceShift

variable {β : Type*} [MeasurableSpace β]
Expand Down
1 change: 0 additions & 1 deletion Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,6 @@ namespace Exchangeability.DeFinetti.ViaKoopman
open MeasureTheory Filter Topology ProbabilityTheory
open Exchangeability.Ergodic
open Exchangeability.PathSpace
open Exchangeability.DeFinetti.MartingaleHelpers (comap_comp_le)
open scoped BigOperators RealInnerProductSpace

variable {α : Type*} [MeasurableSpace α]
Expand Down
1 change: 0 additions & 1 deletion Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@ namespace Exchangeability.DeFinetti.ViaKoopman
open MeasureTheory Filter Topology ProbabilityTheory
open Exchangeability.Ergodic
open Exchangeability.PathSpace
open Exchangeability.DeFinetti.MartingaleHelpers (comap_comp_le)
open scoped BigOperators

variable {α : Type*} [MeasurableSpace α]
Expand Down
4 changes: 2 additions & 2 deletions Exchangeability/DeFinetti/ViaMartingale/RevFiltration.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ lemma revFiltration_antitone (X : ℕ → Ω → α) :
simp only [shiftRV, shiftSeq, Function.comp_apply]
congr 1
omega
rw [h_comp]
exact comap_comp_le (shiftRV X m) (shiftSeq k) measurable_shiftSeq
rw [h_comp, ← MeasurableSpace.comap_comp]
exact MeasurableSpace.comap_mono measurable_shiftSeq.comap_le

end Exchangeability.DeFinetti.ViaMartingale