Order-connected sets are null-measurable

This file proves that order-connected sets in ℝⁿ under the pointwise order are null-measurable. Recall that x ≤ y iff ∀ i, x i ≤ y i, and s is order-connected iff ∀ x y ∈ s, ∀ z, x ≤ z → z ≤ y → z ∈ s.

Main declarations

• Set.OrdConnected.null_frontier: The frontier of an order-connected set in ℝⁿ has measure 0.

Notes

We prove null-measurability in ℝⁿ with the ∞-metric, but this transfers directly to ℝⁿ with the Euclidean metric because they have the same measurable sets.

Null-measurability can't be strengthened to measurability because any antichain (and in particular any subset of the antidiagonal {(x, y) | x + y = 0}) is order-connected.

Sketch proof

1. To show an order-connected set is null-measurable, it is enough to show it has null frontier.
2. Since an order-connected set is the intersection of its upper and lower closure, it's enough to show that upper and lower sets have null frontier.
3. WLOG let's prove it for an upper set s.
4. By the Lebesgue density theorem, it is enough to show that any frontier point x of s is not a Lebesgue point, namely we want the density of s over small balls centered at x to not tend to either 0 or 1.
5. This is true, since by the upper setness of s we can intercalate a ball of radius δ / 4 in s intersected with the upper quadrant of the ball of radius δ centered at x (recall that the balls are taken in the ∞-norm, so they are cubes), and another ball of radius δ / 4 in sᶜ and the lower quadrant of the ball of radius δ centered at x.

TODO

Generalize so that it also applies to ℝ × ℝ, for example.

theorem IsUpperSet.null_frontier {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : IsUpperSet s) : MeasureTheory.volume (frontier s) = 0

theorem IsLowerSet.null_frontier {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : IsLowerSet s) : MeasureTheory.volume (frontier s) = 0

theorem Set.OrdConnected.null_frontier {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : s.OrdConnected) : MeasureTheory.volume (frontier s) = 0

theorem Set.OrdConnected.nullMeasurableSet {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : s.OrdConnected) : MeasureTheory.NullMeasurableSet s MeasureTheory.volume

theorem IsAntichain.volume_eq_zero {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} [Nonempty ι] (hs : IsAntichain (fun (x1 x2 : ι → ℝ) => x1 ≤ x2) s) : MeasureTheory.volume s = 0