Blumberg theorem

Stream: Is there code for X?

[Niels Voss]

Do we have a proof of the Blumberg theorem, which states that for every $f : \mathbb{R} \to \mathbb{R}$ there exists a dense subset $D \subseteq \mathbb{R}$ such that the restriction $f|_D : D \to \mathbb{R}$ is continuous?

[Junyan Xu]

I didn't know the theorem before and it's quite interesting. I looked up Wikipedia and this is particularly interesting:

It was constructed by taking the disjoint union of two compact Hausdorff spaces, one of which could be proven to be non-Blumberg if the Continuum Hypothesis was true, the other if it was false.

[Matt Diamond]

PDF of the original paper: https://www.ams.org/journals/tran/1922-024-02/S0002-9947-1922-1501216-9/S0002-9947-1922-1501216-9.pdf

Theorem III is the "Blumberg theorem" (though I suppose that they're all technically Blumberg theorems...)

[Johan Commelin]

Junyan Xu said:

I didn't know the theorem before and it's quite interesting. I looked up Wikipedia and this is particularly interesting:

It was constructed by taking the disjoint union of two compact Hausdorff spaces, one of which could be proven to be non-Blumberg if the Continuum Hypothesis was true, the other if it was false.

Sounds like the proof relied on the law of excluded middle :rofl:

[Kevin Buzzard]

I think that without LEM you might well have several competing definitions of $\mathbb{R}$...

[Niels Voss]

Would this counterexample of a Compact Hausdorff Space that is non-Blumberg be a good candidate for Mathlib Counterexamples?

[Kevin Buzzard]

Who knew that open subsets of the plane were called "I-regions" in 1919?!

[Kevin Buzzard]

Theorem III does not state what the original post in this thread says; the D is a dense subset of the plane, not the line (so in fact I'm slightly confused; if D is the complement of the graph of f then Theorem III as stated in this 1919 paper seems vacuously true...)

[Kevin Buzzard]

This paper is much easier to read: https://www.ams.org/journals/proc/1960-011-04/S0002-9939-1960-0146310-1/S0002-9939-1960-0146310-1.pdf (it definitely looks formalizable, it's only 3 pages and is almost entirely self-contained)

[Mario Carneiro]

Kevin Buzzard said:

Theorem III does not state what the original post in this thread says; the D is a dense subset of the plane, not the line (so in fact I'm slightly confused; if D is the complement of the graph of f then Theorem III as stated in this 1919 paper seems vacuously true...)

I think in that particular theorem $f:\mathbb{R}\times \mathbb{R}\to\mathbb{R}$

[Mario Carneiro]

and it seems the $\mathbb{R}\times\mathbb{R}$ was later generalized to what we are now calling Blumberg's theorem

[Niels Voss]

This paper is much easier to read: https://www.ams.org/journals/proc/1960-011-04/S0002-9939-1960-0146310-1/S0002-9939-1960-0146310-1.pdf (it definitely looks formalizable, it's only 3 pages and is almost entirely self-contained)

I think I looked at that earlier and it definitely seems simpler. The paper seems to create new definitions of a point being meager relative to a subset of a space, a space being of the "homogenous second category", the concept of a heavy point, and something called an almost continuous function

[Mario Carneiro]

Do we have the definitions of first and second Baire category? (I really don't like those names...)

[Niels Voss]

I think those are just meager and nonmeager, respectively?

[Mario Carneiro]

looks like the mathlib notion is docs#residual, although I'm not sure exactly which terminologies it equates to

[Mario Carneiro]

Oh, there is also docs#IsMeagre and some spelling clash of "meagre" / "meager" in docstrings

[Niels Voss]

Based on some quick wikipedia reading, I think residual == comeager, which means that the complement is meager. comeager is not the same as nonmeager. I think we have an IsMeager predicate somewhere in Mathlib?

[Niels Voss]

Yeah that sounds right

[Niels Voss]

Should I make a PR to change all 8 instances of "meager" in docstrings to "meagre"?

[Mario Carneiro]

should there generally be a preference for US vs UK spelling in mathlib? Seems like a dedicated discussion is in order

[Mario Carneiro]

I'm glad the 8 "misspellings" were there or I wouldn't have found the definition at all

[Mario Carneiro]

all spellings should definitely be mentioned in the declaration docstring

[Niels Voss]

Yeah, that sounds reasonable. The docstring should also mention "Baire first category". There are 40 instances of "meagre" (based on the result of rg meager --ignore-case -c) and 8 instances of "meager". I actually initially used "meager" because I live in the US, but I think we should use the one that appears most often in math literature.

[Mario Carneiro]

Agreed. ...Do we know which one that is?