feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable (#16976)

Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero.

As a corollary, antichains in `ℝⁿ` have measure zero.

Co-authored-by: @JasonKYi

Author: YaelDillies

src/analysis/normed/order/upper_lower.lean

@@ -23,10 +23,11 @@ are measurable.
 -/
 
 open function metric set
+open_locale pointwise
 
 variables {α ι : Type*}
 
-section metric_space
+section normed_ordered_group
 variables [normed_ordered_group α] {s : set α}
 
 @[to_additive is_upper_set.thickening]
@@ -49,12 +50,22 @@ protected lemma is_lower_set.cthickening' (hs : is_lower_set s) (ε : ℝ) :
   is_lower_set (cthickening ε s) :=
 by { rw cthickening_eq_Inter_thickening'', exact is_lower_set_Inter₂ (λ δ hδ, hs.thickening' _) }
 
-end metric_space
+@[to_additive upper_closure_interior_subset]
+lemma upper_closure_interior_subset' (s : set α) :
+  (upper_closure (interior s) : set α) ⊆ interior (upper_closure s) :=
+upper_closure_min (interior_mono subset_upper_closure) (upper_closure s).upper.interior
+
+@[to_additive lower_closure_interior_subset]
+lemma lower_closure_interior_subset' (s : set α) :
+  (upper_closure (interior s) : set α) ⊆ interior (upper_closure s) :=
+upper_closure_min (interior_mono subset_upper_closure) (upper_closure s).upper.interior
+
+end normed_ordered_group
 
 /-! ### `ℝⁿ` -/
 
 section finite
-variables [finite ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+variables [finite ι] {s : set (ι → ℝ)} {x y : ι → ℝ}
 
 lemma is_upper_set.mem_interior_of_forall_lt (hs : is_upper_set s) (hx : x ∈ closure s)
   (h : ∀ i, x i < y i) :
@@ -99,7 +110,78 @@ end
 end finite
 
 section fintype
-variables [fintype ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+variables [fintype ι] {s t : set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+
+-- TODO: Generalise those lemmas so that they also apply to `ℝ` and `euclidean_space ι ℝ`
+lemma dist_inf_sup (x y : ι → ℝ) : dist (x ⊓ y) (x ⊔ y) = dist x y :=
+begin
+  refine congr_arg coe (finset.sup_congr rfl $ λ i _, _),
+  simp only [real.nndist_eq', sup_eq_max, inf_eq_min, max_sub_min_eq_abs, pi.inf_apply,
+    pi.sup_apply, real.nnabs_of_nonneg, abs_nonneg, real.to_nnreal_abs],
+end
+
+lemma dist_mono_left : monotone_on (λ x, dist x y) (Ici y) :=
+begin
+  refine λ y₁ hy₁ y₂ hy₂ hy, nnreal.coe_le_coe.2 (finset.sup_mono_fun $ λ i _, _),
+  rw [real.nndist_eq, real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)),
+    real.nndist_eq, real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))],
+  exact real.to_nnreal_mono (sub_le_sub_right (hy _) _),
+end
+
+lemma dist_mono_right : monotone_on (dist x) (Ici x) :=
+by simpa only [dist_comm] using dist_mono_left
+
+lemma dist_anti_left : antitone_on (λ x, dist x y) (Iic y) :=
+begin
+  refine λ y₁ hy₁ y₂ hy₂ hy, nnreal.coe_le_coe.2 (finset.sup_mono_fun $ λ i _, _),
+  rw [real.nndist_eq', real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
+    real.nndist_eq', real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))],
+  exact real.to_nnreal_mono (sub_le_sub_left (hy _) _),
+end
+
+lemma dist_anti_right : antitone_on (dist x) (Iic x) :=
+by simpa only [dist_comm] using dist_anti_left
+
+lemma dist_le_dist_of_le (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) : dist a₁ b₁ ≤ dist a₂ b₂ :=
+(dist_mono_right h₁ (h₁.trans hb) hb).trans $
+  dist_anti_left (ha.trans $ h₁.trans hb) (h₁.trans hb) ha
+
+protected lemma metric.bounded.bdd_below : bounded s → bdd_below s :=
+begin
+  rintro ⟨r, hr⟩,
+  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty,
+  { exact bdd_below_empty },
+  { exact ⟨x - const _ r, λ y hy i, sub_le_comm.1
+      (abs_sub_le_iff.1 $ (dist_le_pi_dist _ _ _).trans $ hr _ hx _ hy).1⟩ }
+end
+
+protected lemma metric.bounded.bdd_above : bounded s → bdd_above s :=
+begin
+  rintro ⟨r, hr⟩,
+  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty,
+  { exact bdd_above_empty },
+  { exact ⟨x + const _ r, λ y hy i, sub_le_iff_le_add'.1 $
+      (abs_sub_le_iff.1 $ (dist_le_pi_dist _ _ _).trans $ hr _ hx _ hy).2⟩ }
+end
+
+protected lemma bdd_below.bounded : bdd_below s → bdd_above s → bounded s :=
+begin
+  rintro ⟨a, ha⟩ ⟨b, hb⟩,
+  refine ⟨dist a b, λ x hx y hy, _⟩,
+  rw ←dist_inf_sup,
+  exact dist_le_dist_of_le (le_inf (ha hx) $ ha hy) inf_le_sup (sup_le (hb hx) $ hb hy),
+end
+
+protected lemma bdd_above.bounded : bdd_above s → bdd_below s → bounded s := flip bdd_below.bounded
+
+lemma bounded_iff_bdd_below_bdd_above : bounded s ↔ bdd_below s ∧ bdd_above s :=
+⟨λ h, ⟨h.bdd_below, h.bdd_above⟩, λ h, h.1.bounded h.2⟩
+
+lemma bdd_below.bounded_inter (hs : bdd_below s) (ht : bdd_above t) : bounded (s ∩ t) :=
+(hs.mono $ inter_subset_left _ _).bounded $ ht.mono $ inter_subset_right _ _
+
+lemma bdd_above.bounded_inter (hs : bdd_above s) (ht : bdd_below t) : bounded (s ∩ t) :=
+(hs.mono $ inter_subset_left _ _).bounded $ ht.mono $ inter_subset_right _ _
 
 lemma is_upper_set.exists_subset_ball (hs : is_upper_set s) (hx : x ∈ closure s) (hδ : 0 < δ) :
   ∃ y, closed_ball y (δ/4) ⊆ closed_ball x δ ∧ closed_ball y (δ/4) ⊆ interior s :=
@@ -140,3 +222,74 @@ begin
 end
 
 end fintype
+
+section finite
+variables [finite ι] {s t : set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+
+lemma is_antichain.interior_eq_empty [nonempty ι] (hs : is_antichain (≤) s) : interior s = ∅ :=
+begin
+  casesI nonempty_fintype ι,
+  refine eq_empty_of_forall_not_mem (λ x hx, _),
+  have hx' := interior_subset hx,
+  rw [mem_interior_iff_mem_nhds, metric.mem_nhds_iff] at hx,
+  obtain ⟨ε, hε, hx⟩ := hx,
+  refine hs.not_lt hx' (hx _) (lt_add_of_pos_right _ (by positivity : 0 < const ι (ε / 2))),
+  simpa [const, @pi_norm_const ι ℝ _ _ _ (ε / 2), abs_of_nonneg hε.lt.le],
+end
+
+/-!
+#### Note
+
+The closure and frontier of an antichain might not be antichains. Take for example the union
+of the open segments from `(0, 2)` to `(1, 1)` and from `(2, 1)` to `(3, 0)`. `(1, 1)` and `(2, 1)`
+are comparable and both in the closure/frontier.
+-/
+
+protected lemma is_closed.upper_closure (hs : is_closed s) (hs' : bdd_below s) :
+  is_closed (upper_closure s : set (ι → ℝ)) :=
+begin
+  casesI nonempty_fintype ι,
+  refine is_seq_closed.is_closed (λ f x hf hx, _),
+  choose g hg hgf using hf,
+  obtain ⟨a, ha⟩ := hx.bdd_above_range,
+  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.bounded_inter
+    bdd_above_Iic) (λ n, ⟨hg n, (hgf _).trans $  ha $ mem_range_self _⟩),
+  exact ⟨b, closure_minimal (inter_subset_left _ _) hs hb,
+    le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_at_top) $ λ _, hgf _⟩,
+end
+
+protected lemma is_closed.lower_closure (hs : is_closed s) (hs' : bdd_above s) :
+  is_closed (lower_closure s : set (ι → ℝ)) :=
+begin
+  casesI nonempty_fintype ι,
+  refine is_seq_closed.is_closed (λ f x hf hx, _),
+  choose g hg hfg using hf,
+  haveI : bounded_ge_nhds_class ℝ := by apply_instance,
+  obtain ⟨a, ha⟩ := hx.bdd_below_range,
+  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.bounded_inter
+    bdd_below_Ici) (λ n, ⟨hg n, (ha $ mem_range_self _).trans $ hfg _⟩),
+  exact ⟨b, closure_minimal (inter_subset_left _ _) hs hb,
+    le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_at_top) hbf $ λ _, hfg _⟩,
+end
+
+protected lemma is_clopen.upper_closure (hs : is_clopen s) (hs' : bdd_below s) :
+  is_clopen (upper_closure s : set (ι → ℝ)) :=
+⟨hs.1.upper_closure, hs.2.upper_closure hs'⟩
+
+protected lemma is_clopen.lower_closure (hs : is_clopen s) (hs' : bdd_above s) :
+  is_clopen (lower_closure s : set (ι → ℝ)) :=
+⟨hs.1.lower_closure, hs.2.lower_closure hs'⟩
+
+lemma closure_upper_closure_comm (hs : bdd_below s) :
+  closure (upper_closure s : set (ι → ℝ)) = upper_closure (closure s) :=
+(closure_minimal (upper_closure_anti subset_closure) $
+  is_closed_closure.upper_closure hs.closure).antisymm $
+    upper_closure_min (closure_mono subset_upper_closure) (upper_closure s).upper.closure
+
+lemma closure_lower_closure_comm (hs : bdd_above s) :
+  closure (lower_closure s : set (ι → ℝ)) = lower_closure (closure s) :=
+(closure_minimal (lower_closure_mono subset_closure) $
+  is_closed_closure.lower_closure hs.closure).antisymm $
+    lower_closure_min (closure_mono subset_lower_closure) (lower_closure s).lower.closure
+
+end finite

src/data/real/nnreal.lean

@@ -822,6 +822,8 @@ lemma nnabs_coe (x : ℝ≥0) : nnabs x = x := by simp
 lemma coe_to_nnreal_le (x : ℝ) : (to_nnreal x : ℝ) ≤ |x| :=
 max_le (le_abs_self _) (abs_nonneg _)
 
+@[simp] lemma to_nnreal_abs (x : ℝ) : |x|.to_nnreal = x.nnabs := nnreal.coe_injective $ by simp
+
 lemma cast_nat_abs_eq_nnabs_cast (n : ℤ) :
   (n.nat_abs : ℝ≥0) = nnabs n :=
 by { ext, rw [nnreal.coe_nat_cast, int.cast_nat_abs, real.coe_nnabs] }

src/measure_theory/order/upper_lower.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2022 Yaël Dillies, Kexing Ying. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Kexing Ying
+-/
+import analysis.normed.order.upper_lower
+import logic.lemmas
+import measure_theory.covering.besicovitch_vector_space
+
+/-!
+# 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.ord_connected.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.
+
+## TODO
+
+Generalize so that it also applies to `ℝ × ℝ`, for example.
+-/
+
+open filter measure_theory metric set
+open_locale topology
+
+variables {ι : Type*} [fintype ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+
+/-- If we can fit a small ball inside a set `s` intersected with any neighborhood of `x`, then the
+density of `s` near `x` is not `0`. Along with `aux₁`, this proves that `x` is a Lebesgue point of
+`s`. This will be used to prove that the frontier of an order-connected set is null. -/
+private lemma aux₀
+  (h : ∀ δ, 0 < δ → ∃ y, closed_ball y (δ/4) ⊆ closed_ball x δ ∧ closed_ball y (δ/4) ⊆ interior s) :
+  ¬ tendsto (λ r, volume (closure s ∩ closed_ball x r) / volume (closed_ball x r)) (𝓝[>] 0)
+    (𝓝 0) :=
+begin
+  choose f hf₀ hf₁ using h,
+  intros H,
+  obtain ⟨ε, hε, hε', hε₀⟩ := exists_seq_strict_anti_tendsto_nhds_within (0 : ℝ),
+  refine not_eventually.2 (frequently_of_forall $ λ _, lt_irrefl $
+    ennreal.of_real $ 4⁻¹ ^ fintype.card ι)
+   ((tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds _).mono $ λ n, lt_of_le_of_lt _),
+  swap,
+  refine (ennreal.div_le_div_right (volume.mono $ subset_inter
+    ((hf₁ _ $ hε' n).trans interior_subset_closure) $ hf₀ _ $ hε' n) _).trans_eq' _,
+  dsimp,
+  have := hε' n,
+  rw [real.volume_pi_closed_ball, real.volume_pi_closed_ball, ←ennreal.of_real_div_of_pos, ←div_pow,
+    mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div],
+  all_goals { positivity },
+end
+
+/-- If we can fit a small ball inside a set `sᶜ` intersected with any neighborhood of `x`, then the
+density of `s` near `x` is not `1`. Along with `aux₀`, this proves that `x` is a Lebesgue point of
+`s`. This will be used to prove that the frontier of an order-connected set is null. -/
+private lemma aux₁
+  (h : ∀ δ, 0 < δ →
+    ∃ y, closed_ball y (δ/4) ⊆ closed_ball x δ ∧ closed_ball y (δ/4) ⊆ interior sᶜ) :
+  ¬ tendsto (λ r, volume (closure s ∩ closed_ball x r) / volume (closed_ball x r)) (𝓝[>] 0)
+    (𝓝 1) :=
+begin
+  choose f hf₀ hf₁ using h,
+  intros H,
+  obtain ⟨ε, hε, hε', hε₀⟩ := exists_seq_strict_anti_tendsto_nhds_within (0 : ℝ),
+  refine not_eventually.2 (frequently_of_forall $ λ _, lt_irrefl $
+    1 - ennreal.of_real (4⁻¹ ^ fintype.card ι))
+    ((tendsto.eventually_lt tendsto_const_nhds (H.comp hε₀) $
+    ennreal.sub_lt_self ennreal.one_ne_top one_ne_zero _).mono $ λ n, lt_of_le_of_lt' _),
+  swap,
+  refine (ennreal.div_le_div_right (volume.mono _) _).trans_eq _,
+  { exact closed_ball x (ε n) \ closed_ball (f (ε n) $ hε' n) (ε n / 4) },
+  { rw diff_eq_compl_inter,
+    refine inter_subset_inter_left _ _,
+    rw [subset_compl_comm, ←interior_compl],
+    exact hf₁ _ _ },
+  dsimp,
+  have := hε' n,
+  rw [measure_diff (hf₀ _ _) _ ((real.volume_pi_closed_ball _ _).trans_ne ennreal.of_real_ne_top),
+    real.volume_pi_closed_ball, real.volume_pi_closed_ball,  ennreal.sub_div (λ _ _, _),
+    ennreal.div_self _ ennreal.of_real_ne_top, ←ennreal.of_real_div_of_pos, ←div_pow,
+    mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div],
+  all_goals { positivity <|> measurability },
+end
+
+lemma is_upper_set.null_frontier (hs : is_upper_set s) : volume (frontier s) = 0 :=
+begin
+  refine eq_bot_mono (volume.mono $ λ x hx, _)
+    (besicovitch.ae_tendsto_measure_inter_div_of_measurable_set _ is_closed_closure.measurable_set),
+  { exact s },
+  by_cases x ∈ closure s; simp [h],
+  { exact aux₁ (λ _, hs.compl.exists_subset_ball $ frontier_subset_closure $
+      by rwa frontier_compl) },
+  { exact aux₀ (λ _, hs.exists_subset_ball $ frontier_subset_closure hx) }
+end
+
+lemma is_lower_set.null_frontier (hs : is_lower_set s) : volume (frontier s) = 0 :=
+begin
+  refine eq_bot_mono (volume.mono $ λ x hx, _)
+    (besicovitch.ae_tendsto_measure_inter_div_of_measurable_set _ is_closed_closure.measurable_set),
+  { exact s },
+  by_cases x ∈ closure s; simp [h],
+  { exact aux₁ (λ _, hs.compl.exists_subset_ball $ frontier_subset_closure $
+      by rwa frontier_compl) },
+  { exact aux₀ (λ _, hs.exists_subset_ball $ frontier_subset_closure hx) }
+end
+
+lemma set.ord_connected.null_frontier (hs : s.ord_connected) : volume (frontier s) = 0 :=
+begin
+  rw ← hs.upper_closure_inter_lower_closure,
+  refine le_bot_iff.1 ((volume.mono $ (frontier_inter_subset _ _).trans $ union_subset_union
+    (inter_subset_left _ _) $ inter_subset_right _ _).trans $ (measure_union_le _ _).trans_eq _),
+  rw [(upper_set.upper _).null_frontier, (lower_set.lower _).null_frontier, zero_add, bot_eq_zero],
+end
+
+protected lemma set.ord_connected.null_measurable_set (hs : s.ord_connected) :
+  null_measurable_set s :=
+null_measurable_set_of_null_frontier hs.null_frontier
+
+lemma is_antichain.volume_eq_zero [nonempty ι] (hs : is_antichain (≤) s) : volume s = 0 :=
+le_bot_iff.1 $ (volume.mono $ by { rw [←closure_diff_interior, hs.interior_eq_empty, diff_empty],
+  exact subset_closure }).trans_eq hs.ord_connected.null_frontier

src/order/bounds/basic.lean

@@ -62,6 +62,8 @@ def is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
 
 lemma mem_upper_bounds : a ∈ upper_bounds s ↔ ∀ x ∈ s, x ≤ a := iff.rfl
 lemma mem_lower_bounds : a ∈ lower_bounds s ↔ ∀ x ∈ s, a ≤ x := iff.rfl
+lemma mem_upper_bounds_iff_subset_Iic : a ∈ upper_bounds s ↔ s ⊆ Iic a := iff.rfl
+lemma mem_lower_bounds_iff_subset_Ici : a ∈ lower_bounds s ↔ s ⊆ Ici a := iff.rfl
 
 lemma bdd_above_def : bdd_above s ↔ ∃ x, ∀ y ∈ s, y ≤ x := iff.rfl
 lemma bdd_below_def : bdd_below s ↔ ∃ x, ∀ y ∈ s, x ≤ y := iff.rfl

src/topology/algebra/order/upper_lower.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import algebra.order.upper_lower
 import topology.algebra.group.basic
+import topology.order.basic
 
 /-!
 # Topological facts about upper/lower/order-connected sets
@@ -46,7 +47,33 @@ instance ordered_comm_group.to_has_upper_lower_closure [ordered_comm_group α]
   is_open_upper_closure := λ s hs, by { rw [←mul_one s, ←mul_upper_closure], exact hs.mul_right },
   is_open_lower_closure := λ s hs, by { rw [←mul_one s, ←mul_lower_closure], exact hs.mul_right } }
 
-variables [preorder α] [has_upper_lower_closure α] {s : set α}
+variables [preorder α]
+
+section order_closed_topology
+variables [order_closed_topology α] {s : set α}
+
+@[simp] lemma upper_bounds_closure (s : set α) :
+  upper_bounds (closure s : set α) = upper_bounds s :=
+ext $ λ a, by simp_rw [mem_upper_bounds_iff_subset_Iic, is_closed_Iic.closure_subset_iff]
+
+@[simp] lemma lower_bounds_closure (s : set α) :
+  lower_bounds (closure s : set α) = lower_bounds s :=
+ext $ λ a, by simp_rw [mem_lower_bounds_iff_subset_Ici, is_closed_Ici.closure_subset_iff]
+
+@[simp] lemma bdd_above_closure : bdd_above (closure s) ↔ bdd_above s :=
+by simp_rw [bdd_above, upper_bounds_closure]
+
+@[simp] lemma bdd_below_closure : bdd_below (closure s) ↔ bdd_below s :=
+by simp_rw [bdd_below, lower_bounds_closure]
+
+alias bdd_above_closure ↔ bdd_above.of_closure bdd_above.closure
+alias bdd_below_closure ↔ bdd_below.of_closure bdd_below.closure
+
+attribute [protected] bdd_above.closure bdd_below.closure
+
+end order_closed_topology
+
+variables [has_upper_lower_closure α] {s : set α}
 
 protected lemma is_upper_set.closure : is_upper_set s → is_upper_set (closure s) :=
 has_upper_lower_closure.is_upper_set_closure _