feat(data/set/intervals): define intervals and prove basic properties (…

…leanprover-community#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/order_functions.lean

@@ -275,6 +275,16 @@ begin
   { refl }
 end
 
+lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = abs (a - b) :=
+begin
+  cases le_total a b with ab ba,
+  { rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub], rwa sub_nonpos },
+  { rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg], exact sub_nonneg_of_le ba }
+end
+
+lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = abs (b - a) :=
+by { rw [abs_sub], exact max_sub_min_eq_abs' _ _ }
+
 end decidable_linear_ordered_comm_group
 
 section decidable_linear_ordered_semiring

src/analysis/convex/basic.lean

@@ -103,6 +103,9 @@ end
 lemma segment_eq_Icc' (a b : ℝ) : [a, b] = Icc (min a b) (max a b) :=
 by cases le_total a b; [skip, rw segment_symm]; simp [segment_eq_Icc, *]
 
+lemma segment_eq_interval (a b : ℝ) : segment a b = interval a b :=
+segment_eq_Icc' _ _
+
 lemma mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b, a + c] ↔ x ∈ [b, c] :=
 begin
   rw [segment_eq_image', segment_eq_image'],
@@ -737,7 +740,7 @@ f.is_linear.image_convex_hull
 lemma finset.center_mass_mem_convex_hull (t : finset ι) {w : ι → ℝ} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
   (hws : 0 < t.sum w) {z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) :
   t.center_mass w z ∈ convex_hull s :=
-(convex_convex_hull s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull s $ hz i hi) 
+(convex_convex_hull s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull s $ hz i hi)
 
 -- TODO : Do we need other versions of the next lemma?
 

src/data/indicator_function.lean

@@ -38,6 +38,9 @@ variables [has_zero β] {s t : set α} {f g : α → β} {a : α}
 @[reducible]
 def indicator (s : set α) (f : α → β) : α → β := λ x, if x ∈ s then f x else 0
 
+@[simp] lemma indicator_apply (s : set α) (f : α → β) (a : α) :
+  indicator s f a = if a ∈ s then f a else 0 := rfl
+
 @[simp] lemma indicator_of_mem (h : a ∈ s) (f : α → β) : indicator s f a = f a := if_pos h
 
 @[simp] lemma indicator_of_not_mem (h : a ∉ s) (f : α → β) : indicator s f a = 0 := if_neg h
@@ -59,6 +62,17 @@ variable {β}
 lemma indicator_indicator (s t : set α) (f : α → β) : indicator s (indicator t f) = indicator (s ∩ t) f :=
 funext $ λx, by { simp only [indicator], split_ifs, repeat {simp * at * {contextual := tt}} }
 
+lemma indicator_comp_of_zero {γ} [has_zero γ] {g : β → γ} (hg : g 0 = 0) :
+  indicator s (g ∘ f) = λ a, indicator (f '' s) g (indicator s f a) :=
+begin
+  funext, simp only [indicator],
+  split_ifs with h h',
+  { refl },
+  { have := mem_image_of_mem _ h, contradiction },
+  { rwa eq_comm },
+  refl
+end
+
 lemma indicator_preimage (s : set α) (f : α → β) (B : set β) :
   (indicator s f)⁻¹' B = s ∩ f ⁻¹' B ∪ (-s) ∩ (λa:α, (0:β)) ⁻¹' B :=
 by { rw [indicator, if_preimage] }
@@ -150,9 +164,30 @@ end
 
 end add_group
 
+section mul_zero_class
+variables [mul_zero_class β] {s t : set α} {f g : α → β} {a : α}
+
+lemma indicator_mul (s : set α) (f g : α → β) :
+  indicator s (λa, f a * g a) = λa, indicator s f a * indicator s g a :=
+by { funext, simp only [indicator], split_ifs, { refl }, rw mul_zero }
+
+end mul_zero_class
+
 section order
 variables [has_zero β] [preorder β] {s t : set α} {f g : α → β} {a : α}
 
+lemma indicator_nonneg' (h : a ∈ s → 0 ≤ f a) : 0 ≤ indicator s f a :=
+by { rw indicator_apply, split_ifs with as, { exact h as }, refl }
+
+lemma indicator_nonneg (h : ∀ a ∈ s, 0 ≤ f a) : ∀ a, 0 ≤ indicator s f a :=
+λ a, indicator_nonneg' (h a)
+
+lemma indicator_nonpos' (h : a ∈ s → f a ≤ 0) : indicator s f a ≤ 0 :=
+by { rw indicator_apply, split_ifs with as, { exact h as }, refl }
+
+lemma indicator_nonpos (h : ∀ a ∈ s, f a ≤ 0) : ∀ a, indicator s f a ≤ 0 :=
+λ a, indicator_nonpos' (h a)
+
 lemma indicator_le_indicator (h : f a ≤ g a) : indicator s f a ≤ indicator s g a :=
 by { simp only [indicator], split_ifs with ha, { exact h }, refl }
 

src/data/set/intervals/basic.lean

@@ -556,11 +556,20 @@ end sup
 
 section both
 
-variables {α : Type u} [lattice α] [ht : is_total α (≤)] {a₁ a₂ b₁ b₂ : α}
+variables {α : Type u} [lattice α] [ht : is_total α (≤)] {a b c a₁ a₂ b₁ b₂ : α}
 
 lemma Icc_inter_Icc : Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂) :=
 by simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]; ac_refl
 
+@[simp] lemma Icc_inter_Icc_eq_singleton (hab : a ≤ b) (hbc : b ≤ c) :
+  Icc a b ∩ Icc b c = {b} :=
+begin
+  rw [Icc_inter_Icc],
+  convert Icc_self b,
+  exact sup_of_le_right hab,
+  exact inf_of_le_left hbc
+end
+
 include ht
 
 lemma Ico_inter_Ico : Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂) :=

src/data/set/intervals/default.lean

@@ -1 +1 @@
-import data.set.intervals.basic data.set.intervals.disjoint
+import data.set.intervals.basic data.set.intervals.disjoint data.set.intervals.unordered_interval

src/data/set/intervals/unordered_interval.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2020 Zhouhang Zhou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zhouhang Zhou
+-/
+
+import data.set.intervals.basic order.bounds
+
+/-!
+# Intervals without endpoints ordering
+
+In any decidable linear order `α`, we define the set of elements lying between two elements `a` and
+`b` as `Icc (min a b) (max a b)`.
+
+`Icc a b` requires the assumption `a ≤ b` to be meaningful, which is sometimes inconvenient. The
+interval as defined in this file is always the set of things lying between `a` and `b`, regardless
+of the relative order of `a` and `b`.
+
+For real numbers, `Icc (min a b) (max a b)` is the same as `segment a b`.
+
+## Notation
+
+We use the localized notation `[a, b]` for `interval a b`. One can open the locale `interval` to
+make the notation available.
+
+-/
+
+universe u
+
+namespace set
+
+section decidable_linear_order
+
+variables {α : Type u} [decidable_linear_order α] {a a₁ a₂ b b₁ b₂ x : α}
+
+/-- `interval a b` is the set of elements lying between `a` and `b`, with `a` and `b` included. -/
+def interval (a b : α) := Icc (min a b) (max a b)
+
+localized "notation `[`a `, ` b `]` := interval a b" in interval
+
+@[simp] lemma interval_of_le (h : a ≤ b) : [a, b] = Icc a b :=
+by rw [interval, min_eq_left h, max_eq_right h]
+
+@[simp] lemma interval_of_ge (h : b ≤ a) : [a, b] = Icc b a :=
+by { rw [interval, min_eq_right h, max_eq_left h] }
+
+lemma interval_swap (a b : α) : [a, b] = [b, a] :=
+or.elim (le_total a b) (by simp {contextual := tt}) (by simp {contextual := tt})
+
+lemma interval_of_lt (h : a < b) : [a, b] = Icc a b :=
+interval_of_le (le_of_lt h)
+
+lemma interval_of_gt (h : b < a) : [a, b] = Icc b a :=
+interval_of_ge (le_of_lt h)
+
+lemma interval_of_not_le (h : ¬ a ≤ b) : [a, b] = Icc b a :=
+interval_of_gt (lt_of_not_ge h)
+
+lemma interval_of_not_ge (h : ¬ b ≤ a) : [a, b] = Icc a b :=
+interval_of_lt (lt_of_not_ge h)
+
+@[simp] lemma interval_self : [a, a] = {a} :=
+set.ext $ by simp [le_antisymm_iff, and_comm]
+
+@[simp] lemma nonempty_interval : set.nonempty [a, b] :=
+by { simp only [interval, min_le_iff, le_max_iff, nonempty_Icc], left, left, refl }
+
+@[simp] lemma left_mem_interval : a ∈ [a, b] :=
+by { rw [interval, mem_Icc], exact ⟨min_le_left _ _, le_max_left _ _⟩ }
+
+@[simp] lemma right_mem_interval : b ∈ [a, b] :=
+by { rw interval_swap, exact left_mem_interval }
+
+lemma Icc_subset_interval : Icc a b ⊆ [a, b] :=
+by { assume x h, rwa interval_of_le, exact le_trans h.1 h.2 }
+
+lemma Icc_subset_interval' : Icc b a ⊆ [a, b] :=
+by { rw interval_swap, apply Icc_subset_interval }
+
+lemma mem_interval_of_le (ha : a ≤ x) (hb : x ≤ b) : x ∈ [a, b] :=
+Icc_subset_interval ⟨ha, hb⟩
+
+lemma mem_interval_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [a, b] :=
+Icc_subset_interval' ⟨hb, ha⟩
+
+lemma interval_subset_interval (h₁ : a₁ ∈ [a₂, b₂]) (h₂ : b₁ ∈ [a₂, b₂]) : [a₁, b₁] ⊆ [a₂, b₂] :=
+Icc_subset_Icc (le_min h₁.1 h₂.1) (max_le h₁.2 h₂.2)
+
+lemma interval_subset_interval_iff_mem : [a₁, b₁] ⊆ [a₂, b₂] ↔ a₁ ∈ [a₂, b₂] ∧ b₁ ∈ [a₂, b₂] :=
+iff.intro (λh, ⟨h left_mem_interval, h right_mem_interval⟩) (λ h, interval_subset_interval h.1 h.2)
+
+lemma interval_subset_interval_iff_le :
+  [a₁, b₁] ⊆ [a₂, b₂] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂ :=
+by { rw [interval, interval, Icc_subset_Icc_iff], exact min_le_max }
+
+lemma interval_subset_interval_right (h : x ∈ [a, b]) : [x, b] ⊆ [a, b] :=
+interval_subset_interval h right_mem_interval
+
+lemma interval_subset_interval_left (h : x ∈ [a, b]) : [a, x] ⊆ [a, b] :=
+interval_subset_interval left_mem_interval h
+
+lemma bdd_below_bdd_above_iff_subset_interval (s : set α) :
+  bdd_below s ∧ bdd_above s ↔ ∃ a b, s ⊆ [a, b] :=
+begin
+  rw [bdd_below_bdd_above_iff_subset_Icc],
+  split,
+  { rintro ⟨a, b, h⟩, exact ⟨a, b, λ x hx, Icc_subset_interval (h hx)⟩ },
+  { rintro ⟨a, b, h⟩, exact ⟨min a b, max a b, h⟩ }
+end
+
+end decidable_linear_order
+
+open_locale interval
+
+section ordered_comm_group
+
+variables {α : Type u} [decidable_linear_ordered_comm_group α] {a b x y : α}
+
+/-- If `[x, y]` is a subinterval of `[a, b]`, then the distance between `x` and `y`
+is less than or equal to that of `a` and `b` -/
+lemma abs_sub_le_of_subinterval (h : [x, y] ⊆ [a, b]) : abs (y - x) ≤ abs (b - a) :=
+begin
+  rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs],
+  rw [interval_subset_interval_iff_le] at h,
+  exact sub_le_sub h.2 h.1,
+end
+
+/-- If `x ∈ [a, b]`, then the distance between `a` and `x` is less than or equal to
+that of `a` and `b`  -/
+lemma abs_sub_left_of_mem_interval (h : x ∈ [a, b]) : abs (x - a) ≤ abs (b - a) :=
+abs_sub_le_of_subinterval (interval_subset_interval_left h)
+
+/-- If `x ∈ [a, b]`, then the distance between `x` and `b` is less than or equal to
+that of `a` and `b`  -/
+lemma abs_sub_right_of_mem_interval (h : x ∈ [a, b]) : abs (b - x) ≤ abs (b - a) :=
+abs_sub_le_of_subinterval (interval_subset_interval_right h)
+
+end ordered_comm_group
+
+end set

src/measure_theory/borel_space.lean

@@ -271,6 +271,13 @@ lemma is_measurable_Ioc : is_measurable (Ioc a b) := is_measurable_Ioi.inter is_
 lemma is_measurable_Ico : is_measurable (Ico a b) := is_measurable_Ici.inter is_measurable_Iio
 lemma is_measurable_Icc : is_measurable (Icc a b) := is_measurable_of_is_closed is_closed_Icc
 
+open_locale interval
+
+lemma is_measurable_interval
+  {α} [decidable_linear_order α] [topological_space α] [order_closed_topology α] {a b : α} :
+  is_measurable [a, b] :=
+is_measurable_Icc
+
 end order_closed_topology
 
 lemma measurable.is_lub {α} [topological_space α] [linear_order α]

src/measure_theory/lebesgue_measure.lean

@@ -233,6 +233,14 @@ instance : measure_space ℝ :=
 @[simp] theorem lebesgue_to_outer_measure :
   (measure_space.μ : measure ℝ).to_outer_measure = lebesgue_outer := rfl
 
+end measure_theory
+
+open measure_theory
+
+section volume
+
+open_locale interval
+
 theorem real.volume_val (s) : volume s = lebesgue_outer s := rfl
 local attribute [simp] real.volume_val
 
@@ -241,6 +249,27 @@ local attribute [simp] real.volume_val
 @[simp] lemma real.volume_Ioo {a b : ℝ} : volume (Ioo a b) = of_real (b - a) := by simp
 @[simp] lemma real.volume_singleton {a : ℝ} : volume ({a} : set ℝ) = 0 := by simp
 
+@[simp] lemma real.volume_interval {a b : ℝ} : volume [a, b] = of_real (abs (b - a)) :=
+begin
+  rw [interval, real.volume_Icc],
+  congr,
+  exact max_sub_min_eq_abs _ _
+end
+
+open metric
+
+lemma real.volume_lt_top_of_bounded {s : set ℝ} (h : bounded s) : volume s < ⊤ :=
+begin
+  rw [real.bounded_iff_bdd_below_bdd_above, bdd_below_bdd_above_iff_subset_interval] at h,
+  rcases h with ⟨a, b, h⟩,
+  calc volume s ≤ volume [a, b] : volume_mono h
+    ... < ⊤ : by { rw real.volume_interval, exact ennreal.coe_lt_top }
+end
+
+lemma real.volume_lt_top_of_compact {s : set ℝ} (h : compact s) : volume s < ⊤ :=
+real.volume_lt_top_of_bounded (bounded_of_compact h)
+
+end volume
 /-
 section vitali
 
@@ -265,5 +294,3 @@ sorry
 
 end vitali
 -/
-
-end measure_theory

src/order/bounds.lean

@@ -279,6 +279,14 @@ lemma bdd_above_of_bdd_above_of_monotone {f : α → β} (hf : monotone f) : bdd
 lemma bdd_below_of_bdd_below_of_monotone {f : α → β} (hf : monotone f) : bdd_below s → bdd_below (f '' s)
 | ⟨C, hC⟩ := ⟨f C, by rintro y ⟨x, x_bnd, rfl⟩; exact hf (hC x_bnd)⟩
 
+lemma bdd_below_iff_subset_Ici (s : set α) : bdd_below s ↔ ∃ a, s ⊆ Ici a := iff.rfl
+
+lemma bdd_above_iff_subset_Iic (s : set α) : bdd_above s ↔ ∃ a, s ⊆ Iic a := iff.rfl
+
+lemma bdd_below_bdd_above_iff_subset_Icc (s : set α) :
+  bdd_below s ∧ bdd_above s ↔ ∃ a b, s ⊆ Icc a b :=
+by simp [Ici_inter_Iic.symm, subset_inter_iff, bdd_below_iff_subset_Ici, bdd_above_iff_subset_Iic]
+
 end preorder
 
 /--When there is a global maximum, every set is bounded above.-/