[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable

src/algebra/order/upper_lower.lean

@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import algebra.order.group
+import order.upper_lower
+
+/-!
+# Algebraic operations on upper/lower sets
+
+Upper/lower sets are preserved under pointwise algebraic operations in ordered groups.
+-/
+
+alias ne_of_eq_of_ne ← eq.trans_ne
+alias ne_of_ne_of_eq ← ne.trans_eq
+
+open function set
+open_locale pointwise
+
+section
+variables {α : Type*} [mul_one_class α] [has_lt α] [contravariant_class α α (*) (<)] {a b : α}
+
+@[to_additive] lemma one_lt_of_lt_mul_right : a < a * b → 1 < b :=
+by simpa only [mul_one] using (lt_of_mul_lt_mul_left' : a * 1 < a * b → 1 < b)
+
+end
+
+section
+variables {α : Type*} [mul_one_class α] [preorder α] [contravariant_class α α (*) (<)]
+  [has_exists_mul_of_le α] {a b : α}
+
+@[to_additive] lemma exists_one_lt_mul_of_lt' (h : a < b) : ∃ c, 1 < c ∧ a * c = b :=
+by { obtain ⟨c, rfl⟩ := exists_mul_of_le h.le, exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩ }
+
+end
+
+section finite
+variables {α ι : Type*} [linear_ordered_semifield α] [has_exists_add_of_le α] [finite ι]
+  {x y : ι → α}
+
+lemma pi.exists_forall_pos_add_lt (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i :=
+begin
+  casesI nonempty_fintype ι,
+  casesI is_empty_or_nonempty ι,
+  { exact ⟨1, zero_lt_one, is_empty_elim⟩ },
+  choose ε hε hxε using λ i, exists_pos_add_of_lt' (h i),
+  obtain rfl : x + ε = y := funext hxε,
+  have hε : 0 < finset.univ.inf' finset.univ_nonempty ε := (finset.lt_inf'_iff _).2 (λ i _, hε _),
+  exact ⟨_, half_pos hε, λ i, add_lt_add_left ((half_lt_self hε).trans_le $ finset.inf'_le _ $
+    finset.mem_univ _) _⟩,
+end
+
+end finite
+
+section ordered_comm_monoid
+variables {α : Type*} [ordered_comm_monoid α] {s : set α} {x : α}
+
+@[to_additive] lemma is_upper_set.smul_subset (hs : is_upper_set s) (hx : 1 ≤ x) : x • s ⊆ s :=
+smul_set_subset_iff.2 $ λ y, hs $ le_mul_of_one_le_left' hx
+
+@[to_additive] lemma is_lower_set.smul_subset (hs : is_lower_set s) (hx : x ≤ 1) : x • s ⊆ s :=
+smul_set_subset_iff.2 $ λ y, hs $ mul_le_of_le_one_left' hx
+
+end ordered_comm_monoid
+
+section ordered_comm_group
+variables {α : Type*} [ordered_comm_group α] {s t : set α} {a : α}
+
+@[to_additive] lemma is_upper_set.smul (hs : is_upper_set s) : is_upper_set (a • s) :=
+begin
+  rintro _ y hxy ⟨x, hx, rfl⟩,
+  exact mem_smul_set_iff_inv_smul_mem.2 (hs (le_inv_mul_iff_mul_le.2 hxy) hx),
+end
+
+@[to_additive] lemma is_lower_set.smul (hs : is_lower_set s) : is_lower_set (a • s) :=
+hs.of_dual.smul
+
+@[to_additive] lemma set.ord_connected.smul (hs : s.ord_connected) : (a • s).ord_connected :=
+⟨begin
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ z hz,
+  exact mem_smul_set_iff_inv_smul_mem.2
+    (hs.out hx hy ⟨le_inv_mul_iff_mul_le.2 hz.1, inv_mul_le_iff_le_mul.2 hz.2⟩),
+end⟩
+
+@[to_additive] lemma is_upper_set.mul_left (ht : is_upper_set t) : is_upper_set (s * t) :=
+by { rw [←smul_eq_mul, ←bUnion_smul_set], exact is_upper_set_Union₂ (λ x hx, ht.smul) }
+
+@[to_additive] lemma is_upper_set.mul_right (hs : is_upper_set s) : is_upper_set (s * t) :=
+by { rw mul_comm, exact hs.mul_left }
+
+@[to_additive] lemma is_lower_set.mul_left (ht : is_lower_set t) : is_lower_set (s * t) :=
+ht.of_dual.mul_left
+
+@[to_additive] lemma is_lower_set.mul_right (hs : is_lower_set s) : is_lower_set (s * t) :=
+hs.of_dual.mul_right
+
+@[to_additive] lemma is_upper_set.div_left (ht : is_upper_set t) : is_lower_set (s / t) :=
+begin
+  rw [←image2_div, ←Union_image_left],
+  refine is_lower_set_Union₂ (λ x hx, _),
+  rintro _ z hyz ⟨y, hy, rfl⟩,
+  exact ⟨x / z, ht (by rwa le_div'') hy, div_div_cancel _ _⟩,
+end
+
+@[to_additive] lemma is_upper_set.div_right (hs : is_upper_set s) : is_upper_set (s / t) :=
+begin
+  rw [←image2_div, ←Union_image_right],
+  refine is_upper_set_Union₂ (λ x hx, _),
+  rintro _ z hyz ⟨y, hy, rfl⟩,
+  exact ⟨x * z, hs (by rwa ←div_le_iff_le_mul') hy, mul_div_cancel''' _ _⟩,
+end
+
+@[to_additive] lemma is_lower_set.div_left (ht : is_lower_set t) : is_upper_set (s / t) :=
+ht.of_dual.div_left
+
+@[to_additive] lemma is_lower_set.div_right (hs : is_lower_set s) : is_lower_set (s / t) :=
+hs.of_dual.div_right
+
+namespace upper_set
+
+@[to_additive] instance : has_mul (upper_set α) := ⟨λ s t, ⟨s * t, s.2.mul_right⟩⟩
+@[to_additive] instance : has_div (upper_set α) := ⟨λ s t, ⟨s / t, s.2.div_right⟩⟩
+@[to_additive] instance : has_smul α (upper_set α) := ⟨λ a s, ⟨a • s, s.2.smul⟩⟩
+
+@[simp, norm_cast, to_additive]
+lemma coe_smul (a : α) (s : upper_set α) : (↑(a • s) : set α) = a • s := rfl
+@[simp, norm_cast, to_additive]
+lemma coe_mul (s t : upper_set α) : (↑(s * t) : set α) = s * t := rfl
+@[simp, norm_cast, to_additive]
+lemma coe_div (s t : upper_set α) : (↑(s / t) : set α) = s / t := rfl
+
+@[to_additive] instance : mul_action α (upper_set α) := set_like.coe_injective.mul_action _ coe_smul
+
+end upper_set
+
+namespace lower_set
+
+@[to_additive] instance : has_mul (lower_set α) := ⟨λ s t, ⟨s * t, s.2.mul_right⟩⟩
+@[to_additive] instance : has_div (lower_set α) := ⟨λ s t, ⟨s / t, s.2.div_right⟩⟩
+@[to_additive] instance : has_smul α (lower_set α) := ⟨λ a s, ⟨a • s, s.2.smul⟩⟩
+
+@[simp, norm_cast, to_additive]
+lemma coe_smul (a : α) (s : lower_set α) : (↑(a • s) : set α) = a • s := rfl
+@[simp, norm_cast, to_additive]
+lemma coe_mul (s t : lower_set α) : (↑(s * t) : set α) = s * t := rfl
+@[simp, norm_cast, to_additive]
+lemma coe_div (s t : lower_set α) : (↑(s / t) : set α) = s / t := rfl
+
+@[to_additive] instance : mul_action α (lower_set α) := set_like.coe_injective.mul_action _ coe_smul
+
+end lower_set
+
+end ordered_comm_group

src/measure_theory/order/upper_lower.lean

@@ -0,0 +1,115 @@
+/-
+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 measure_theory.covering.besicovitch_vector_space
+import topology.algebra.order.upper_lower
+
+/-!
+# Order-connected sets are null-measurable
+
+This file proves that order-connected sets in `ℝⁿ` under the pointwise order are measurable.
+
+## Main declarations
+
+* `set.ord_connected.null_frontier`: The frontier of an order-connected set in `ℝⁿ` has measure `0`.
+
+## Notes
+
+We prove measurability in `ℝⁿ` with the `∞`-metric, but this transfers directly to `ℝⁿ` with the
+Euclidean metric because they have the same measurable sets.
+
+## TODO
+
+Generalize so that it also applies to `ℝ × ℝ`, for example.
+-/
+
+open filter measure_theory metric set
+open_locale topological_space
+
+variables {ι : Type*} [fintype ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+
+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
+
+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

src/order/upper_lower.lean

@@ -217,6 +217,26 @@ lemma not_bdd_below_Iio : ¬ bdd_below (Iio a) := (is_lower_set_Iio _).not_bdd_b
 end no_min_order
 end preorder
 
+section partial_order
+variables [partial_order α] {s : set α}
+
+lemma is_upper_set_iff_forall_lt : is_upper_set s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s :=
+forall_congr $ λ a, by simp [le_iff_eq_or_lt, or_imp_distrib, forall_and_distrib]
+
+lemma is_lower_set_iff_forall_lt : is_lower_set s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s :=
+forall_congr $ λ a, by simp [le_iff_eq_or_lt, or_imp_distrib, forall_and_distrib]
+
+lemma is_upper_set_iff_Ioi_subset : is_upper_set s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s :=
+by simp [is_upper_set_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]
+
+lemma is_lower_set_iff_Iio_subset : is_lower_set s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s :=
+by simp [is_lower_set_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]
+
+alias is_upper_set_iff_Ioi_subset ↔ is_upper_set.Ioi_subset _
+alias is_lower_set_iff_Iio_subset ↔ is_lower_set.Iio_subset _
+
+end partial_order
+
 /-! ### Bundled upper/lower sets -/
 
 section has_le
@@ -591,12 +611,6 @@ def lower_closure (s : set α) : lower_set α :=
 lemma subset_upper_closure : s ⊆ upper_closure s := λ x hx, ⟨x, hx, le_rfl⟩
 lemma subset_lower_closure : s ⊆ lower_closure s := λ x hx, ⟨x, hx, le_rfl⟩
 
-lemma upper_closure_min (h : s ⊆ t) (ht : is_upper_set t) : ↑(upper_closure s) ⊆ t :=
-λ a ⟨b, hb, hba⟩, ht hba $ h hb
-
-lemma lower_closure_min (h : s ⊆ t) (ht : is_lower_set t) : ↑(lower_closure s) ⊆ t :=
-λ a ⟨b, hb, hab⟩, ht hab $ h hb
-
 @[simp] lemma upper_set.infi_Ici (s : set α) : (⨅ a ∈ s, upper_set.Ici a) = upper_closure s :=
 by { ext, simp }
 
@@ -606,11 +620,11 @@ by { ext, simp }
 lemma gc_upper_closure_coe :
   galois_connection (to_dual ∘ upper_closure : set α → (upper_set α)ᵒᵈ) (coe ∘ of_dual) :=
 λ s t, ⟨λ h, subset_upper_closure.trans $ upper_set.coe_subset_coe.2 h,
-  λ h, upper_closure_min h t.upper⟩
+  λ h a ⟨b, hb, hba⟩, t.upper hba $ h hb⟩
 
 lemma gc_lower_closure_coe : galois_connection (lower_closure : set α → lower_set α) coe :=
 λ s t, ⟨λ h, subset_lower_closure.trans $ lower_set.coe_subset_coe.2 h,
-  λ h, lower_closure_min h t.lower⟩
+  λ h a ⟨b, hb, hab⟩, t.lower hab $ h hb⟩
 
 /-- `upper_closure` forms a reversed Galois insertion with the coercion from upper sets to sets. -/
 def gi_upper_closure_coe :