From afcbf98c3d8badf2b0170863e210fb21c5980b2e Mon Sep 17 00:00:00 2001 From: Francesco Chotuck Date: Wed, 26 Aug 2026 20:02:45 +0100 Subject: [PATCH] feat(StandardBorel): BorelSpace instances for sum and sigma types --- BrownianMotion/Auxiliary/StandardBorel.lean | 30 ++++++++++++++------- 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/BrownianMotion/Auxiliary/StandardBorel.lean b/BrownianMotion/Auxiliary/StandardBorel.lean index 08883cf2..17eb94e2 100644 --- a/BrownianMotion/Auxiliary/StandardBorel.lean +++ b/BrownianMotion/Auxiliary/StandardBorel.lean @@ -4,23 +4,35 @@ public import Mathlib.MeasureTheory.Constructions.Polish.Basic @[expose] public section +open Topology + variable {α β ι : Type*} {γ : ι → Type*} [Countable ι] [MeasurableSpace α] [MeasurableSpace β] [∀ n, MeasurableSpace (γ n)] instance BorelSpace.sum [TopologicalSpace α] [TopologicalSpace β] [BorelSpace α] [BorelSpace β] : BorelSpace (α ⊕ β) := by - constructor - rw [Sum.instMeasurableSpace] - refine le_antisymm ?_ ?_ - · sorry - · refine MeasurableSpace.generateFrom_le fun t ht ↦ ?_ - simp only [isOpen_sum_iff, Set.mem_ofPred_eq] at ht - rw [measurableSet_sum_iff] - exact ⟨ht.1.measurableSet, ht.2.measurableSet⟩ + refine ⟨le_antisymm ?_ ?_⟩ + · borelize (α ⊕ β) + intro s hs + obtain ⟨hl, hr⟩ := measurableSet_sum_iff.mp hs + rw [← Set.image_preimage_inl_union_image_preimage_inr s] + refine MeasurableSet.union ?_ ?_ + · exact IsOpenEmbedding.inl.measurableEmbedding.measurableSet_image' hl + · exact IsOpenEmbedding.inr.measurableEmbedding.measurableSet_image' hr + · refine MeasurableSpace.generateFrom_le fun t ht ↦ measurableSet_sum_iff.mpr ?_ + exact (isOpen_sum_iff.mp ht).imp IsOpen.measurableSet IsOpen.measurableSet instance BorelSpace.sigma [∀ n, TopologicalSpace (γ n)] [∀ n, BorelSpace (γ n)] : BorelSpace ((n : ι) × γ n) := by - sorry + refine ⟨le_antisymm ?_ ?_⟩ + · borelize ((n : ι) × γ n) + intro s hs + rw [← Set.iUnion_image_preimage_sigma_mk_eq_self s] + refine MeasurableSet.iUnion fun n ↦ MeasurableEmbedding.measurableSet_image' ?_ ?_ + · exact IsOpenEmbedding.sigmaMk.measurableEmbedding + · exact MeasurableSpace.measurableSet_iInf.mp hs n + · refine MeasurableSpace.generateFrom_le fun t ht ↦ ?_ + exact MeasurableSpace.measurableSet_iInf.mpr fun n ↦ (isOpen_sigma_iff.mp ht n).measurableSet /-- A sum of two standard Borel spaces is standard Borel. -/ instance StandardBorelSpace.sum [StandardBorelSpace α] [StandardBorelSpace β] :