From b1abe23ae96fef89ad30d9f4362c307f72a55010 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 16 Oct 2023 09:24:06 +0000 Subject: [PATCH] =?UTF-8?q?feat(measure=5Ftheory/order/upper=5Flower):=20O?= =?UTF-8?q?rder-connected=20sets=20in=20`=E2=84=9D=E2=81=BF`=20are=20measu?= =?UTF-8?q?rable=20(#16976)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/analysis/normed/order/upper_lower.lean | 161 +++++++++++++++++++- src/data/real/nnreal.lean | 2 + src/measure_theory/order/upper_lower.lean | 131 ++++++++++++++++ src/order/bounds/basic.lean | 2 + src/topology/algebra/order/upper_lower.lean | 29 +++- 5 files changed, 320 insertions(+), 5 deletions(-) create mode 100644 src/measure_theory/order/upper_lower.lean diff --git a/src/analysis/normed/order/upper_lower.lean b/src/analysis/normed/order/upper_lower.lean index c834d2d671ddc..a081b70aa9623 100644 --- a/src/analysis/normed/order/upper_lower.lean +++ b/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 diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean index cca419cf48609..47dba7306a2d2 100644 --- a/src/data/real/nnreal.lean +++ b/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] } diff --git a/src/measure_theory/order/upper_lower.lean b/src/measure_theory/order/upper_lower.lean new file mode 100644 index 0000000000000..d6bc49a4cfffa --- /dev/null +++ b/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 diff --git a/src/order/bounds/basic.lean b/src/order/bounds/basic.lean index 6add0bb14d555..ab986bd7f2fd4 100644 --- a/src/order/bounds/basic.lean +++ b/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 diff --git a/src/topology/algebra/order/upper_lower.lean b/src/topology/algebra/order/upper_lower.lean index 792ad0b431a15..c1286acac2cdc 100644 --- a/src/topology/algebra/order/upper_lower.lean +++ b/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 _