borel sigma-algebra & quotient topology

Stream: maths

[Yury G. Kudryashov]

What assumptions do I need on s : Setoid X, where {X : Type _} [TopologicalSpace X] so that (borel X).map (Quotient.mk s) = borel (Quotient s)?

[Yury G. Kudryashov]

E.g., is it true for a (nice) action of a group on a topological space? Is it true for the quotient of a group by a (closed? countable?) subgroup?

[Jireh Loreaux]

Doesn't this fail even in really nice scenarios, like projection from R^2 to R?

[Jireh Loreaux]

@Sebastien Gouezel

[Anatole Dedecker]

I guess this would at least be true if the quotient is a covering map, does that sound right?

[Felix Weilacher]

Jireh Loreaux said:

Doesn't this fail even in really nice scenarios, like projection from R^2 to R?

This will hold for any projection p : X × Y → X. The quotient topology on X is the original topology on X. Meanwhile if p^{-1} U = U × Y is Borel in X × Y, then U × {y} is Borel in X × {y} for your favorite y, so U is Borel in X.

[Felix Weilacher]

Yury G. Kudryashov said:

E.g., is it true for a (nice) action of a group on a topological space? Is it true for the quotient of a group by a (closed? countable?) subgroup?

It's not true for the quotient of R by Q. The quotient topology on R/Q is the indiscrete one, but for example singletons are in the LHS since their preimages in R are countable. I might believe that a quotient by a closed subgroup always works though.

The same idea applies to the irrational rotation (a Z action on the unit circle) which is about as nice an interesting group action as you can ask for.

[Felix Weilacher]

I'm not confident, but I think this equality holds if X is compact and s is closed as a subset of X^2. The upshot there is that the saturation of a closed set is still closed.

[Yury G. Kudryashov]

What if we require that there exists a fundamental domain? Which definition of a fundamental domain will work?

[Yury G. Kudryashov]

E.g., how can we quickly prove it for the projection from real numbers to the circle?

[Heather Macbeth]

What context have you encountered the map of the sigma-algebra in? In such contexts I have always worked with the borel sigma-algebras both upstairs and downstairs, and not encountered the pushforward-to-downstairs-of-the-upstairs-borel-sigma-algebra at all.

[Yury G. Kudryashov]

You temporarily disable the quotient instance for MeasurableSpace in MeasureTheory.Integral.Periodic. IMHO, it's better to reuse the instance and prove BorelSpace.

[Heather Macbeth]

Interesting -- actually I had been meaning to ask at some point whether there's even any point at all in having the quotient instance for MeasurableSpace! Is it mathematically meaningful in general?

[Heather Macbeth]

(I don't think it's used in the library, except for well-behaved topological space quotients where there is also the "borel sigma-algebra of the quotient topology" available.)

[Yury G. Kudryashov]

Another approach is to remove it completely ;)

[Yury G. Kudryashov]

AFAIR, I added it some time ago. I don't remember why.

[Yury G. Kudryashov]

(or it was someone else?)

[Heather Macbeth]

Do you know whether you had a textbook reference or invented it yourself?

[Yury G. Kudryashov]

I definitely didn't have a textbook reference.

[Yury G. Kudryashov]

I just used the existing map operation.

[Heather Macbeth]

It was indeed you, #10275.

[Yury G. Kudryashov]

In any case, the statement "a set on the circle is measurable iff its preimage under projection is measurable" looks like something we should have.

[Yury G. Kudryashov]

BTW, should we add AddCircle.mk and use it instead of QuotientAddGroup.mk for Coe?

[Yury G. Kudryashov]

Otherwise Lean unfolds AddCircle to the quotient group here and there.

[Felix Weilacher]

Heather Macbeth said:

What context have you encountered the map of the sigma-algebra in? In such contexts I have always worked with the borel sigma-algebras both upstairs and downstairs, and not encountered the pushforward-to-downstairs-of-the-upstairs-borel-sigma-algebra at all.

I'm not saying it should be an instance, but the pushforward is almost always the correct sigma algebra in the study of Borel equivalence relations. For example, such a relation is called smooth if the pushforward makes the quotient standard Borel, and there are many theorems about smoothness that people find interesting. On the other hand in this setting the quotient topology is often just the indiscrete one.

[Yury G. Kudryashov]

@Felix Weilacher I have a similar question. If E is a (finite dimensional) real normed space with Borel sigma-algebra, is it true that nnnorm is a quotient map in the sense of sigma-algebras?

[Yury G. Kudryashov]

More precisely, I need the following: if f : ℝ≥0 → V is a function such that f ∘ nnnorm is docs4#MeasureTheory.AEStronglyMeasurable, is it true that f is AEStronglyMeasurable?

[Yury G. Kudryashov]

If yes (I hope, it's "yes"), what other functions I can take instead of nnnorm here?

[Yury G. Kudryashov]

@Sebastien Gouezel AFAIR, you learned something similar for your very generic formula about change of variables in an integral.

[Felix Weilacher]

Let X and Y be standard Borel spaces and f:X -> Y a Borel surjection. Let s be a subset of Y with f^{-1}(s) measurable. Let t be the complement of s. Then f^{-1}(t) is also measurable, and since s and t are the images of these preimages, they are both analytic. Therefore s is Borel by docs#measure_theory.analytic_set.measurably_separable.

So if I understand what you mean by quotient map (a set in Y measurable iff its preimage is), f is a quotient map.

The norm is certainly a Borel surjection, so I think the answer is yes.

[Felix Weilacher]

Oh, I guess this also tells you that the original question from this thread has a positive answer if X and Quotient s are both Polish, right? If X is a Polish group and you quotient by a closed subgroup this is the case, for example.

[Yury G. Kudryashov]

What about the AEStronglyMeasurable question?

[Yury G. Kudryashov]

No need to answer

[Yury G. Kudryashov]

StronglyMeasurable is the same as Measurable + second countable topology on the range.

[Yury G. Kudryashov]

BTW, does it mean that we can drop measurability assumption on f in docs#measure_theory.integral_map for many more maps φ?

[Yury G. Kudryashov]

What do we need? measurable_set (range φ) + measurable_space.map (set.range_factorization φ) _inst1 = subtype.measurable_space?

[Felix Weilacher]

This isn't an area of the library I'm familiar with so let me make sure I'm following; is the suggestion that we don't need to assume any measurability for f because if one side defaults to 0 thanks to f being non-measurable, the other side will as well?

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

That's the way we drop this assumption if φ is a docs#measurable_embedding (BTW, I made up this term some time ago; is there a better name?)

[Yury G. Kudryashov]

See src#measurable_embedding.integral_map

[Felix Weilacher]

I like the name

[Felix Weilacher]

Yury G. Kudryashov said:

What do we need? measurable_set (range φ) + measurable_space.map (set.range_factorization φ) _inst1 = subtype.measurable_space?

I'm not sure. What if phi is constant?

[Felix Weilacher]

Then this assumption would hold but f phi would be measurable for free even if f was bad right?

[Yury G. Kudryashov]

I will think about it in the morning.

[Yury G. Kudryashov]

We're talking about a.e.-measurability, so we are allowed to change values at a set of measure zero.

[Yury G. Kudryashov]

If φ is a constant, then we just change f to a constant function.

[Felix Weilacher]

i see

[Yury G. Kudryashov]

@Sebastien Gouezel added "a.e." to many definitions so that a function can be integrable on [0, 1] even if it behaves very badly outside of the interval.

[Felix Weilacher]

I think I agree with what you've said, then

[Felix Weilacher]

And if alpha and beta are standard Borel, the second part of your assumption is automatic given measurable_set (range φ) and measurable φ

[Yury G. Kudryashov]

Do we need measurable φ or continuous φ? I know almost nothing about the descriptive set theory and docs#analytic_set.image_of_continuous requires continuity.

[Felix Weilacher]

measurable is enough by docs#measurable.exists_continuous

[Felix Weilacher]

i.e. Borel images of Borel sets are actually analytic

[Yury G. Kudryashov]

:face_palm:

[Felix Weilacher]

BTW, In the near future I'm hoping to add a standard Borel space typeclass which should hopefully make this sort of thing more straightforward by doing away with topologies

[Yury G. Kudryashov]

I guess, this will have to wait till after the port.

[Yury G. Kudryashov]

Felix Weilacher said:

measurable is enough by docs#measurable.exists_continuous

This gives us a finer topology such that φ is continuous. Why s is an analytic set in this topology?

[Felix Weilacher]

s is a subset of the codomain, whose topology does not change

[Yury G. Kudryashov]

Ah, I was thinking about a wrong lemma. Thank you!

[Yury G. Kudryashov]

Hi, I'm stuck again. I have

theorem Measurable.measurable_comp_iff_of_surjective
    [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace Y] [T2Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y]
    [SecondCountableTopology Y] [MeasurableSpace α] {f : X → Y} (hf : Measurable f)
    (hsurj : Surjective f) {g : Y → α} : Measurable (g ∘ f) ↔ Measurable g := _

but when I try to prove

theorem Measurable.aemeasurable_map_iff_of_surjective
    [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace Y] [T2Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y]
    [SecondCountableTopology Y] [MeasurableSpace α] {f : X → Y}
    (hf : Measurable f) (hsurj : Surjective f) {μ : Measure X} {g : Y → α} :
    AEMeasurable g (map f μ) ↔ AEMeasurable (g ∘ f) μ := by
  refine ⟨fun h ↦ h.comp_measurable hf, ?_⟩
  rintro ⟨gf, hgfm, hgf⟩

I get a measurable function gf : X → α that is a.e.-equal to g ∘ f and I need to find a measurable function Y → αthat is (map f μ)-a.e. equal to g.

[Yury G. Kudryashov]

So, there are two issues:

1. The function gf is not guaranteed to factor through f.
2. Even if it factors through f, the image of the set {x | gf x ≠ g (f x)} can be non-measurable and have positive outer measure (at least I can't prove otherwise yet).

[Yury G. Kudryashov]

@Felix Weilacher @Sebastien Gouezel :up:

[Felix Weilacher]

This is very sketchy... don't take my word that it's all correct or optimal

Assume μ is sigma-finite.

• Suppose s : set Y is such that f⁻¹(s) is null-measurable w.r.t. μ. Let b ⊆ f⁻¹(s) be Borel such that f⁻¹(s) ∖ b is μ-null. Let b ⊆ a ⊆ f⁻¹ s be the set of x : X such that f(x) = f(x') for some x' ∈ b. Then a is analytic and f-invariant (a union of fibers).

• Now f '' a ⊆ s is still analytic, so since the pushforward is a sigma-finite Borel measure, it is null-measurable (!). Let c ⊆ f '' a be Borel such that the f '' a ∖ c is pushforward-null.

• Since a was f-invariant. The preimage of this set, which is μ-null, is a ∖ f⁻¹(c). Chaining, we get that f⁻¹(s) \setminus f⁻¹(c) is μ-null. Thus s ∖ c is pushforward null. c was Borel, so s is null-measurable.

• So this shows f is a quotient map for the null-measurable sigma algebras. Since our spaces are second countable, this should be equivalent to what you want.

Unfortunately the fact (!) that analytic sets are null-measurable is nontrivial and we don't have it.

[Felix Weilacher]

Oh, maybe the equivalence at the end also requires the measurable space on alpha to be countably generated?

[Yury G. Kudryashov]

Where can I find the proof of (!)?

[Felix Weilacher]

Kechris has it as Theorem 21.10. That seems to use other stuff we don't have though. The proof here https://www.personal.psu.edu/jsr25/Spring_11/Lecture_Notes/dst_lecture_notes_2011_Regularity-Analytic.pdf
(13.5) seems not too bad.

[Pedro Sánchez Terraf]

Felix Weilacher said:

Kechris has it as Theorem 21.10. That seems to use other stuff we don't have though.

Also 29.C in Kechris provides (the same?) shortcut using covers.

[Yury G. Kudryashov]

Thank you! I'll have a look tonight.

[Yury G. Kudryashov]

#19186

[Yury G. Kudryashov]

I think that I know a proof that doesn't use "analytic -> null-measurable". I'll try to formalize it tonight to see if it works.

[Yury G. Kudryashov]

(I didn't check all the details yet)

[Yury G. Kudryashov]

UPD: no, there was an error. More details after I try to fix it.

[Yury G. Kudryashov]

I tried to use ae_map_iff on a set that was not known to be measurable.

[Yury G. Kudryashov]

In your proof, how do you prove the first step, i.e. that a = f ⁻¹' (f '' s) is an analytic set?

[Felix Weilacher]

That s should be a b.

It is generally true that the pre-image of an analytic set under a Borel measurable map f: X \to Y is analytic. But I don't think we have it in mathlib.
Proof: Let our analytic set be range g, where g is a measurable fn from some Polish space Z. Consider the set of points (x,z) in X \times Z such that f(x) = g(z). This is Borel since f and g are. f ⁻¹' (range g) is the image of this set under projection to X, so it is analytic since projection is Borel measurable.

[Yury G. Kudryashov]

Then I think that I can deduce the theorem from Lusin separation thm. I'll verify once again (much) later tonight.

[Yury G. Kudryashov]

No, I was wrong again. Indeed, this result needs "analytic -> null-measurable".

[Yury G. Kudryashov]

I'm slowly reading prerequisites. I'll ask lots of questions here.

1. Is "Cantor scheme" as in docs#CantorScheme.inducedMap different from Souslin scheme? If not, should we mention one more name in the docs?
2. Is there a reason to use a sigma type instead of docs#PFun ?

[Felix Weilacher]

1. Indeed, a Souslin Scheme is a CantorScheme with \beta = nat. I agree that this should be mentioned in the docs. In real life Cantor Scheme usually means \beta = {0,1}. (I wanted to call this a Scheme in some namespace, but understandably this was not popular.)
2. I'm not sure I can give a good one. I definitely considered using partial functions when writing CantorScheme, but found them more cumbersome.

[Felix Weilacher]

Btw, Pedro mentioned 29.C in Kechris above, which is also at the link below. I think it would be a good approach.

http://homepages.math.uic.edu/~rosendal/WebpagesMathCourses/MATH511-notes/DST%20notes%20-%20Szpilrajn01.pdf

[Felix Weilacher]

This shouldn't be too bad to implement given the CantorScheme framework. "closed under the souslin operation" just means if A: list nat \to X is such that each A s is a MeasurableSet, then range (inducedMap A).2 is a MeasurableSet.

[Felix Weilacher]

Huh, there is also 29.16 in Kechris which does not require sigma finiteness

[Yury G. Kudryashov]

Yes, I'm reading 29.C (and dependencies about Souslin schemes) in Kechris now.

[Yury G. Kudryashov]

I'm going to move parts of the construction that doesn't depend on topology to a new file.

[Felix Weilacher]

which construction?

[Yury G. Kudryashov]

Cantor scheme, PiNat.res