Skip to content

Commit 65b8389

Browse files
YaelDilliesYaelDillies
committed
chore(MeasureTheory/Constructions/Polish): split off embedding into the reals (#15208)
Credit Rémy for leanprover-community/mathlib3#18881
1 parent 5644f0d commit 65b8389

File tree

9 files changed

+76
-66
lines changed

9 files changed

+76
-66
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3069,7 +3069,8 @@ import Mathlib.MeasureTheory.Constructions.Cylinders
30693069
import Mathlib.MeasureTheory.Constructions.EventuallyMeasurable
30703070
import Mathlib.MeasureTheory.Constructions.HaarToSphere
30713071
import Mathlib.MeasureTheory.Constructions.Pi
3072-
import Mathlib.MeasureTheory.Constructions.Polish
3072+
import Mathlib.MeasureTheory.Constructions.Polish.Basic
3073+
import Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
30733074
import Mathlib.MeasureTheory.Constructions.Prod.Basic
30743075
import Mathlib.MeasureTheory.Constructions.Prod.Integral
30753076
import Mathlib.MeasureTheory.Constructions.Projective

‎Mathlib/MeasureTheory/Constructions/Polish.lean‎ renamed to ‎Mathlib/MeasureTheory/Constructions/Polish/Basic.lean‎

Lines changed: 1 addition & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,9 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sébastien Gouëzel, Felix Weilacher
55
-/
6-
import Mathlib.Data.Real.Cardinality
7-
import Mathlib.Topology.MetricSpace.Perfect
86
import Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
97
import Mathlib.Topology.CountableSeparatingOn
8+
import Mathlib.Topology.MetricSpace.Perfect
109

1110
/-!
1211
# The Borel sigma-algebra on Polish spaces
@@ -1005,58 +1004,3 @@ noncomputable def Equiv.measurableEquiv (e : α ≃ β) : α ≃ᵐ β := by
10051004
rwa [e.countable_iff] at h
10061005

10071006
end PolishSpace
1008-
1009-
namespace MeasureTheory
1010-
1011-
variable (α)
1012-
variable [MeasurableSpace α] [StandardBorelSpace α]
1013-
1014-
theorem exists_nat_measurableEquiv_range_coe_fin_of_finite [Finite α] :
1015-
∃ n : ℕ, Nonempty (α ≃ᵐ range ((↑) : Fin n → ℝ)) := by
1016-
obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α
1017-
refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩
1018-
exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)
1019-
1020-
theorem measurableEquiv_range_coe_nat_of_infinite_of_countable [Infinite α] [Countable α] :
1021-
Nonempty (α ≃ᵐ range ((↑) : ℕ → ℝ)) := by
1022-
have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
1023-
Nat.closedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace
1024-
refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩
1025-
refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_
1026-
exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective
1027-
1028-
/-- Any standard Borel space is measurably equivalent to a subset of the reals. -/
1029-
theorem exists_subset_real_measurableEquiv : ∃ s : Set ℝ, MeasurableSet s ∧ Nonempty (α ≃ᵐ s) := by
1030-
by_cases hα : Countable α
1031-
· cases finite_or_infinite α
1032-
· obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
1033-
refine ⟨_, ?_, h_nonempty_equiv⟩
1034-
letI : MeasurableSpace (Fin n) := borel (Fin n)
1035-
haveI : BorelSpace (Fin n) := ⟨rfl⟩
1036-
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
1037-
exact continuous_of_discreteTopology.measurableEmbedding
1038-
(Nat.cast_injective.comp Fin.val_injective)
1039-
· refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
1040-
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
1041-
exact continuous_of_discreteTopology.measurableEmbedding Nat.cast_injective
1042-
· refine
1043-
⟨univ, MeasurableSet.univ,
1044-
⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
1045-
rw [countable_coe_iff]
1046-
exact Cardinal.not_countable_real
1047-
1048-
/-- Any standard Borel space embeds measurably into the reals. -/
1049-
theorem exists_measurableEmbedding_real : ∃ f : α → ℝ, MeasurableEmbedding f := by
1050-
obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α
1051-
exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩
1052-
1053-
/-- A measurable embedding of a standard Borel space into `ℝ`. -/
1054-
noncomputable
1055-
def embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Ω → ℝ :=
1056-
(exists_measurableEmbedding_real Ω).choose
1057-
1058-
lemma measurableEmbedding_embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] :
1059-
MeasurableEmbedding (embeddingReal Ω) :=
1060-
(exists_measurableEmbedding_real Ω).choose_spec
1061-
1062-
end MeasureTheory

‎Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
/-
2+
Copyright (c) 2023 Rémy Degenne. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Rémy Degenne
5+
-/
6+
import Mathlib.Data.Real.Cardinality
7+
import Mathlib.MeasureTheory.Constructions.Polish.Basic
8+
9+
/-!
10+
# A Polish Borel space is measurably equivalent to a set of reals
11+
-/
12+
13+
open Set Function PolishSpace PiNat TopologicalSpace Bornology Metric Filter Topology MeasureTheory
14+
15+
namespace MeasureTheory
16+
variable (α : Type*) [MeasurableSpace α] [StandardBorelSpace α]
17+
18+
theorem exists_nat_measurableEquiv_range_coe_fin_of_finite [Finite α] :
19+
∃ n : ℕ, Nonempty (α ≃ᵐ range ((↑) : Fin n → ℝ)) := by
20+
obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α
21+
refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩
22+
exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)
23+
24+
theorem measurableEquiv_range_coe_nat_of_infinite_of_countable [Infinite α] [Countable α] :
25+
Nonempty (α ≃ᵐ range ((↑) : ℕ → ℝ)) := by
26+
have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
27+
Nat.closedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace
28+
refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩
29+
refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_
30+
exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective
31+
32+
/-- Any standard Borel space is measurably equivalent to a subset of the reals. -/
33+
theorem exists_subset_real_measurableEquiv : ∃ s : Set ℝ, MeasurableSet s ∧ Nonempty (α ≃ᵐ s) := by
34+
by_cases hα : Countable α
35+
· cases finite_or_infinite α
36+
· obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
37+
refine ⟨_, ?_, h_nonempty_equiv⟩
38+
letI : MeasurableSpace (Fin n) := borel (Fin n)
39+
haveI : BorelSpace (Fin n) := ⟨rfl⟩
40+
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
41+
exact continuous_of_discreteTopology.measurableEmbedding
42+
(Nat.cast_injective.comp Fin.val_injective)
43+
· refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
44+
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
45+
exact continuous_of_discreteTopology.measurableEmbedding Nat.cast_injective
46+
· refine
47+
⟨univ, MeasurableSet.univ,
48+
⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
49+
rw [countable_coe_iff]
50+
exact Cardinal.not_countable_real
51+
52+
/-- Any standard Borel space embeds measurably into the reals. -/
53+
theorem exists_measurableEmbedding_real : ∃ f : α → ℝ, MeasurableEmbedding f := by
54+
obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α
55+
exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩
56+
57+
/-- A measurable embedding of a standard Borel space into `ℝ`. -/
58+
noncomputable
59+
def embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Ω → ℝ :=
60+
(exists_measurableEmbedding_real Ω).choose
61+
62+
lemma measurableEmbedding_embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] :
63+
MeasurableEmbedding (embeddingReal Ω) :=
64+
(exists_measurableEmbedding_real Ω).choose_spec
65+
66+
end MeasureTheory

‎Mathlib/MeasureTheory/Function/Jacobian.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
88
import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
99
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
1010
import Mathlib.Analysis.NormedSpace.Pointwise
11-
import Mathlib.MeasureTheory.Constructions.Polish
11+
import Mathlib.MeasureTheory.Constructions.Polish.Basic
1212
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
1313

1414
/-!

‎Mathlib/MeasureTheory/Integral/Periodic.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Yury Kudryashov, Alex Kontorovich, Heather Macbeth
55
-/
66
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
77
import Mathlib.MeasureTheory.Measure.Haar.Quotient
8-
import Mathlib.MeasureTheory.Constructions.Polish
98
import Mathlib.MeasureTheory.Integral.IntervalIntegral
109
import Mathlib.Topology.Algebra.Order.Floor
1110

‎Mathlib/MeasureTheory/Measure/Haar/Quotient.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ Copyright (c) 2022 Alex Kontorovich and Heather Macbeth. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Alex Kontorovich, Heather Macbeth
55
-/
6+
import Mathlib.Algebra.Group.Opposite
7+
import Mathlib.MeasureTheory.Constructions.Polish.Basic
8+
import Mathlib.MeasureTheory.Group.FundamentalDomain
69
import Mathlib.MeasureTheory.Integral.DominatedConvergence
710
import Mathlib.MeasureTheory.Measure.Haar.Basic
8-
import Mathlib.MeasureTheory.Group.FundamentalDomain
9-
import Mathlib.Algebra.Group.Opposite
10-
import Mathlib.MeasureTheory.Constructions.Polish
1111

1212
/-!
1313
# Haar quotient measure

‎Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Rémy Degenne
55
-/
66
import Mathlib.Data.Complex.Abs
7-
import Mathlib.MeasureTheory.Constructions.Polish
87
import Mathlib.MeasureTheory.Measure.GiryMonad
98
import Mathlib.MeasureTheory.Measure.Stieltjes
109
import Mathlib.Analysis.Normed.Order.Lattice

‎Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Mathlib.Probability.Kernel.Disintegration.Basic
88
import Mathlib.Probability.Kernel.Disintegration.CondCdf
99
import Mathlib.Probability.Kernel.Disintegration.Density
1010
import Mathlib.Probability.Kernel.Disintegration.CdfToKernel
11+
import Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
1112

1213
/-!
1314
# Existence of disintegration of measures and kernels for standard Borel spaces

‎Mathlib/Probability/Martingale/Convergence.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ Copyright (c) 2022 Kexing Ying. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kexing Ying
55
-/
6-
import Mathlib.Probability.Martingale.Upcrossing
6+
import Mathlib.MeasureTheory.Constructions.Polish.Basic
77
import Mathlib.MeasureTheory.Function.UniformIntegrable
8-
import Mathlib.MeasureTheory.Constructions.Polish
8+
import Mathlib.Probability.Martingale.Upcrossing
99

1010
/-!
1111

0 commit comments

Comments
 (0)