From 3e56439df51a712e945f73df5150dc66bb2396ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 13 Jul 2021 12:28:40 +0000 Subject: [PATCH] chore(data/set/intervals): relax linear_order to preorder in the proofs of `Ixx_eq_empty_iff` (#8071) The previous formulations of `Ixx_eq_empty(_iff)` are basically a chaining of this formulation plus `not_lt` or `not_le`. But `not_lt` and `not_le` require `linear_order`. Removing them allows relaxing the typeclasses assumptions on `Ixx_eq_empty_iff` and slightly generalising `Ixx_eq_empty`. --- src/analysis/calculus/tangent_cone.lean | 4 +- src/data/set/intervals/basic.lean | 64 +++++++++++++---------- src/data/set/intervals/disjoint.lean | 4 +- src/data/set/intervals/surj_on.lean | 11 ++-- src/measure_theory/interval_integral.lean | 31 ++++++----- 5 files changed, 63 insertions(+), 51 deletions(-) diff --git a/src/analysis/calculus/tangent_cone.lean b/src/analysis/calculus/tangent_cone.lean index c9c5a5b788ba5..bb44709768540 100644 --- a/src/analysis/calculus/tangent_cone.lean +++ b/src/analysis/calculus/tangent_cone.lean @@ -402,12 +402,12 @@ unique_diff_on_convex (convex_Icc a b) $ by simp only [interior_Icc, nonempty_Io lemma unique_diff_on_Ico (a b : ℝ) : unique_diff_on ℝ (Ico a b) := if hab : a < b then unique_diff_on_convex (convex_Ico a b) $ by simp only [interior_Ico, nonempty_Ioo, hab] -else by simp only [Ico_eq_empty (le_of_not_lt hab), unique_diff_on_empty] +else by simp only [Ico_eq_empty hab, unique_diff_on_empty] lemma unique_diff_on_Ioc (a b : ℝ) : unique_diff_on ℝ (Ioc a b) := if hab : a < b then unique_diff_on_convex (convex_Ioc a b) $ by simp only [interior_Ioc, nonempty_Ioo, hab] -else by simp only [Ioc_eq_empty (le_of_not_lt hab), unique_diff_on_empty] +else by simp only [Ioc_eq_empty hab, unique_diff_on_empty] lemma unique_diff_on_Ioo (a b : ℝ) : unique_diff_on ℝ (Ioo a b) := is_open_Ioo.unique_diff_on diff --git a/src/data/set/intervals/basic.lean b/src/data/set/intervals/basic.lean index 6ccd838321aa8..0c3abcffa9972 100644 --- a/src/data/set/intervals/basic.lean +++ b/src/data/set/intervals/basic.lean @@ -156,21 +156,33 @@ nonempty.to_subtype nonempty_Ioi instance nonempty_Iio_subtype [no_bot_order α] : nonempty (Iio a) := nonempty.to_subtype nonempty_Iio -@[simp] lemma Ioo_eq_empty (h : b ≤ a) : Ioo a b = ∅ := -eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₁.trans h₂).not_le h +@[simp] lemma Icc_eq_empty (h : ¬a ≤ b) : Icc a b = ∅ := +eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans hb) -@[simp] lemma Ico_eq_empty (h : b ≤ a) : Ico a b = ∅ := -eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₁.trans_lt h₂).not_le h +@[simp] lemma Ico_eq_empty (h : ¬a < b) : Ico a b = ∅ := +eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans_lt hb) -@[simp] lemma Icc_eq_empty (h : b < a) : Icc a b = ∅ := -eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₁.trans h₂).not_lt h +@[simp] lemma Ioc_eq_empty (h : ¬a < b) : Ioc a b = ∅ := +eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans_le hb) -@[simp] lemma Ioc_eq_empty (h : b ≤ a) : Ioc a b = ∅ := -eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₂.trans h).not_lt h₁ +@[simp] lemma Ioo_eq_empty (h : ¬a < b) : Ioo a b = ∅ := +eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans hb) -@[simp] lemma Ioo_self (a : α) : Ioo a a = ∅ := Ioo_eq_empty $ le_refl _ -@[simp] lemma Ico_self (a : α) : Ico a a = ∅ := Ico_eq_empty $ le_refl _ -@[simp] lemma Ioc_self (a : α) : Ioc a a = ∅ := Ioc_eq_empty $ le_refl _ +@[simp] lemma Icc_eq_empty_of_lt (h : b < a) : Icc a b = ∅ := +Icc_eq_empty h.not_le + +@[simp] lemma Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅ := +Ico_eq_empty h.not_lt + +@[simp] lemma Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ := +Ioc_eq_empty h.not_lt + +@[simp] lemma Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ := +Ioo_eq_empty h.not_lt + +@[simp] lemma Ico_self (a : α) : Ico a a = ∅ := Ico_eq_empty $ lt_irrefl _ +@[simp] lemma Ioc_self (a : α) : Ioc a a = ∅ := Ioc_eq_empty $ lt_irrefl _ +@[simp] lemma Ioo_self (a : α) : Ioo a a = ∅ := Ioo_eq_empty $ lt_irrefl _ lemma Ici_subset_Ici : Ici a ⊆ Ici b ↔ b ≤ a := ⟨λ h, h $ left_mem_Ici, λ h x hx, h.trans hx⟩ @@ -347,6 +359,18 @@ lemma mem_Icc_of_Ioc (h : x ∈ Ioc a b) : x ∈ Icc a b := Ioc_subset_Icc_self lemma mem_Ici_of_Ioi (h : x ∈ Ioi a) : x ∈ Ici a := Ioi_subset_Ici_self h lemma mem_Iic_of_Iio (h : x ∈ Iio a) : x ∈ Iic a := Iio_subset_Iic_self h +lemma Icc_eq_empty_iff : Icc a b = ∅ ↔ ¬a ≤ b := +by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Icc] + +lemma Ico_eq_empty_iff : Ico a b = ∅ ↔ ¬a < b := +by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ico] + +lemma Ioc_eq_empty_iff : Ioc a b = ∅ ↔ ¬a < b := +by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioc] + +lemma Ioo_eq_empty_iff [densely_ordered α] : Ioo a b = ∅ ↔ ¬a < b := +by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo] + end intervals section partial_order @@ -570,20 +594,6 @@ by rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iic] @[simp] lemma Iio_diff_Iio : Iio b \ Iio a = Ico a b := by rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iio] -lemma Ioo_eq_empty_iff [densely_ordered α] : Ioo a b = ∅ ↔ b ≤ a := -⟨λ eq, le_of_not_lt $ λ h, - let ⟨x, h₁, h₂⟩ := exists_between h in - eq_empty_iff_forall_not_mem.1 eq x ⟨h₁, h₂⟩, -Ioo_eq_empty⟩ - -lemma Ico_eq_empty_iff : Ico a b = ∅ ↔ b ≤ a := -⟨λ eq, le_of_not_lt $ λ h, eq_empty_iff_forall_not_mem.1 eq a ⟨le_rfl, h⟩, - Ico_eq_empty⟩ - -lemma Icc_eq_empty_iff : Icc a b = ∅ ↔ b < a := -⟨λ eq, lt_of_not_ge $ λ h, eq_empty_iff_forall_not_mem.1 eq a ⟨le_rfl, h⟩, - Icc_eq_empty⟩ - lemma Ico_subset_Ico_iff (h₁ : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := ⟨λ h, have a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_rfl, h₁⟩, @@ -635,7 +645,7 @@ begin end @[simp] lemma Iio_subset_Iic_iff [densely_ordered α] : Iio a ⊆ Iic b ↔ a ≤ b := -by rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff] +by rw [←diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt] /-! ### Unions of adjacent intervals -/ @@ -1049,7 +1059,7 @@ begin cases le_or_lt a b with hab hab; cases le_or_lt c d with hcd hcd; simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂, - { exact Icc_union_Icc' (le_of_lt h₂) (le_of_lt h₁) }, + { exact Icc_union_Icc' h₂.le h₁.le }, all_goals { simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt] }, end diff --git a/src/data/set/intervals/disjoint.lean b/src/data/set/intervals/disjoint.lean index bc4857ed8671b..7233e21e48990 100644 --- a/src/data/set/intervals/disjoint.lean +++ b/src/data/set/intervals/disjoint.lean @@ -41,8 +41,8 @@ section linear_order variables [linear_order α] {a₁ a₂ b₁ b₂ : α} @[simp] lemma Ico_disjoint_Ico : disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := -by simp only [set.disjoint_iff, subset_empty_iff, Ico_inter_Ico, Ico_eq_empty_iff, - inf_eq_min, sup_eq_max] +by simp_rw [set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, + inf_eq_min, sup_eq_max, not_lt] @[simp] lemma Ioc_disjoint_Ioc : disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by simpa only [dual_Ico] using @Ico_disjoint_Ico (order_dual α) _ a₂ a₁ b₂ b₁ diff --git a/src/data/set/intervals/surj_on.lean b/src/data/set/intervals/surj_on.lean index cf654d516d7c4..06d760b5d1008 100644 --- a/src/data/set/intervals/surj_on.lean +++ b/src/data/set/intervals/surj_on.lean @@ -25,8 +25,7 @@ begin classical, intros p hp, rcases h_surj p with ⟨x, rfl⟩, - refine ⟨x, _, rfl⟩, - simp only [mem_Ioo], + refine ⟨x, mem_Ioo.2 _, rfl⟩, by_contra h, cases not_and_distrib.mp h with ha hb, { exact has_lt.lt.false (lt_of_lt_of_le hp.1 (h_mono (not_lt.mp ha))) }, @@ -37,16 +36,16 @@ lemma surj_on_Ico_of_monotone_surjective (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) : surj_on f (Ico a b) (Ico (f a) (f b)) := begin - rcases lt_or_ge a b with hab|hab, + obtain hab | hab := lt_or_le a b, { intros p hp, rcases mem_Ioo_or_eq_left_of_mem_Ico hp with hp'|hp', { rw hp', - refine ⟨a, left_mem_Ico.mpr hab, rfl⟩ }, + exact ⟨a, left_mem_Ico.mpr hab, rfl⟩ }, { have := surj_on_Ioo_of_monotone_surjective h_mono h_surj a b hp', cases this with x hx, exact ⟨x, Ioo_subset_Ico_self hx.1, hx.2⟩ } }, - { rw Ico_eq_empty (h_mono hab), - exact surj_on_empty f _ }, + { rw Ico_eq_empty (h_mono hab).not_lt, + exact surj_on_empty f _ } end lemma surj_on_Ioc_of_monotone_surjective diff --git a/src/measure_theory/interval_integral.lean b/src/measure_theory/interval_integral.lean index ae76a477c226e..dd17dfc3f0658 100644 --- a/src/measure_theory/interval_integral.lean +++ b/src/measure_theory/interval_integral.lean @@ -721,7 +721,7 @@ begin cases le_total a b with hab hab, { rw [integral_of_le hab, ← integral_indicator measurable_set_Ioc, indicator_eq_self.2 h]; apply_instance }, - { rw [Ioc_eq_empty hab, subset_empty_iff, function.support_eq_empty_iff] at h, + { rw [Ioc_eq_empty hab.not_lt, subset_empty_iff, function.support_eq_empty_iff] at h, simp [h] } end @@ -907,18 +907,18 @@ lemma continuous_on_primitive {f : α → E} {a b : α} [has_no_atoms μ] (h_int : integrable_on f (Icc a b) μ) : continuous_on (λ x, ∫ t in Ioc a x, f t ∂ μ) (Icc a b) := begin - cases le_or_lt a b with H H, + by_cases h : a ≤ b, { have : ∀ x ∈ Icc a b, ∫ (t : α) in Ioc a x, f t ∂μ = ∫ (t : α) in a..x, f t ∂μ, { intros x x_in, - simp_rw [← interval_oc_of_le H, integral_of_le x_in.1] }, + simp_rw [← interval_oc_of_le h, integral_of_le x_in.1] }, rw continuous_on_congr this, intros x₀ hx₀, refine continuous_within_at_primitive (measure_singleton x₀) _, rw interval_integrable_iff, - simp only [H, max_eq_right, min_eq_left], + simp only [h, max_eq_right, min_eq_left], exact h_int.mono Ioc_subset_Icc_self le_rfl }, - { rw Icc_eq_empty H, - apply continuous_on_empty }, + { rw Icc_eq_empty h, + exact continuous_on_empty _ }, end lemma continuous_on_primitive' {f : α → E} {a b : α} [has_no_atoms μ] @@ -968,7 +968,7 @@ lemma integral_eq_zero_iff_of_nonneg_ae ∫ x in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] 0 := begin cases le_total a b with hab hab; - simp only [Ioc_eq_empty hab, empty_union, union_empty] at hf ⊢, + simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢, { exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi }, { rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm] } end @@ -977,13 +977,16 @@ lemma integral_pos_iff_support_of_nonneg_ae' (hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f) (hfi : interval_integrable f μ a b) : 0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (function.support f ∩ Ioc a b) := begin - cases le_total a b with hab hab; - simp only [integral_of_le, integral_of_ge, Ioc_eq_empty, hab, union_empty, empty_union] at hf ⊢, - { rw [set_integral_pos_iff_support_of_nonneg_ae hf hfi.1, iff.comm, and_iff_right_iff_imp], - contrapose!, - intro h, - rw [Ioc_eq_empty h, inter_empty, measure_empty, nonpos_iff_eq_zero] }, - { simp [integral_nonneg_of_ae hf] } + obtain hab | hab := le_total b a; + simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢, + { rw [←not_iff_not, not_and_distrib, not_lt, not_lt, integral_of_ge hab, neg_nonpos], + exact iff_of_true (integral_nonneg_of_ae hf) (or.intro_left _ hab) }, + rw [integral_of_le hab, set_integral_pos_iff_support_of_nonneg_ae hf hfi.1, iff.comm, + and_iff_right_iff_imp], + contrapose!, + intro h, + rw [Ioc_eq_empty h.not_lt, inter_empty, measure_empty], + exact le_refl 0, end lemma integral_pos_iff_support_of_nonneg_ae