Order-connected sets are measurable

Stream: maths

[Yaël Dillies]

Just to announce that Jason and I just finished proving that the frontier of an order-connected set in ℝⁿ has measure zero! This is a three lines remark in *Reverse Kleitman Inequalities*, Bollobas, Leader, Radcliffe, but it rather took us three months and 10 PRs:

• #16955: Positivity extension for ennreal.of_real
• #16956: nhds_within versions of a few lemmas
• #16958: Distance between constant functions
• #16959: Aliases for =-≠ transitivity lemmas
• #16970: Improve a few lemma names
• #16971: Uniform bound in pi types
• #16972: Move norm lemmas about ℝ earlier
• #16973: Algebraic operations on upper sets
• #16975: The closure of an upper set is an upper set
• #16976: Order-connected sets are measurable

[Yaël Dillies]

All PRs but the last three are independent of each other, so feel free to review if you feel like it!

[Scott Morrison]

You have #16973 twice on the list.

[Yaël Dillies]

Whoops, thanks!

[Sebastien Gouezel]

I have just posted it in the PR, but let me repost it here since discussion is more convenient on Zulip. Can you recall what order-connected means here? The concept is clear to me in linear orders, less clear in general orders. In particular, a few examples would help: the PR shows that the set is null-measurable because the boundary has measure zero, but is there an example showing that it could be non-Borel-measurable?

[Yaël Dillies]

Order-connected in ℝⁿ means that for any two points x y ∈ s such that ∀ i, x i ≤ y i, the cube parallel to the axes with a vertex at x and another one at y is a subset of s. So for example a disk is order-connected, but also the union of the negative-positive and positive-negative quadrants of ℝ².

[Yaël Dillies]

I have no example of a non Borel-mesurable order-connected set.

[Yaël Dillies]

Note that our argument essentially proves that antichains in ℝⁿ have measure zero (but that's a bit weaker than what we actually have). In fact, the measure of antichains is subject to research, as you can see in https://arxiv.org/abs/1911.03421.

[Sebastien Gouezel]

So any subset of the antidiagonal in $\mathbb{R}^2$ is order-connected, right? This gives a lot of non-measurable examples.

[Sebastien Gouezel]

I don't understand why a disk is order-connected, though. It contains the points (-1, 0) and (0, 1), but not the whole square with these as endpoints.

[Yaël Dillies]

Oh sorry, I meant a disk in the ∞-metric :grimacing:

[Sebastien Gouezel]

aka a square :-)

[Yaël Dillies]

The Euclidean metric is a lie. Only the ∞-metric exists.

[Heather Macbeth]

I wonder if there's an extension of the divergence theorem version proved by @Yury G. Kudryashov to your order-connected sets. That theorem applies to individual sets of the form
Yaël Dillies said:

for any two points x y ∈ s such that ∀ i, x i ≤ y i, the cube parallel to the axes with a vertex at x and another one at y

[Yaël Dillies]

What is the mathlib statement?

[Heather Macbeth]

docs#box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at

[Heather Macbeth]

or docs#measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable for a less technical version

[Yaël Dillies]

Possibly! but then you would need to make sense of a face of an order-connected set, which at least requires they be bounded (after all, univ is order-connected and msot certainly doesn't have faces).

[Heather Macbeth]

I mean, I wonder if you could prove something closer to the classic statement of the divergence theorem (involving a surface integral over the boundary), which doesn't involve faces.

[Yaël Dillies]

Ahah. So what do you mean by "extension of the divergence theorem version proved by Yury"? If you mean "technically close", I would doubt it, and if you mean "stronger version", I have no idea because we know Yury worked hard to make his assumptions weak.

[Heather Macbeth]

Yury's assumptions are very weak on the functions involved, and very strong on the domains considered. I'm wondering (very speculatively) if you can enlarge the class of applicable domains.

[Yaël Dillies]

You can write any order-connected set as the (most definitely not disjoint) union of the boxes contained within it. Does that help?

[Heather Macbeth]

No. I'm imagining (to repeat, very speculatively) some exhaustion where you add in more and more disjoint but smaller and smaller boxes.

[Yaël Dillies]

That should still work, but sounds hard to put in practice, and I wouldn't say order-connectedness is the right concept here (it's not even preserved by 90° rotations).

[Yaël Dillies]

I guess the same criticism applies to order-connected -> null-measurable.

[Heather Macbeth]

Yaël Dillies said:

That should still work

You're already more sure than I am, then :)

[Yaël Dillies]

In the sense that you can write an order-connected set as a union of disjoint boxes in this way! I don't actually know whether the measure theory machinery follows.

[Heather Macbeth]

Anyway, you can do that kind of exhaustion for many sets (at a minimum, all open sets), but I guess what the order-connectedness gives you is that you don't need to think very hard in making it. You can always just grab two endpoints in the set and their associated box is in the set.

[Yaël Dillies]

Yes, and then you can split the original set minus the box you removed along the planes of the box you removed, which gives you 3 ^ dimension - 1 sets that are all order-connected.

[Junyan Xu]

I wonder why docs#set.ord_connected is a class while the simpler docs#set.nonempty etc. are not ...

[Yaël Dillies]

I think it's because it appears as an argument in some instances. Granted, those should probably use fact instead.