Zulip Chat Archive

Stream: Is there code for X?

Topic: intervals, abs and shifts


view this post on Zulip Damiano Testa (Dec 17 2020 at 07:17):

In the course of reviewing a PR (#5361), I needed the lemmas below. Do they already appear? What would be a good home? As I have not used very much the side of mathlib with Iccs and the like, I do not really know where they could go.

Any suggestions would be very much appreciated!

/-- A lemma relating a compact interval and its shifts. -/
lemma sub_mem_Icc_iff (α i y : ) : (y - α  Icc (- i) i  y  Icc (α - i) (α + i)) :=
λ a,
  sub_le_iff_le_add.mpr (neg_le_sub_iff_le_add.mp a.1), sub_le_iff_le_add.mp (sub_le.mpr a.2)⟩,
  λ a, neg_le_sub_iff_le_add.mpr (sub_le_iff_le_add.mp a.1) , sub_le_iff_le_add'.mpr a.2⟩⟩

/-- A lemma describing a compact interval via absolute values. -/
lemma abs_le_iff_mem_Icc (α i y : ) : (abs (y - α)  i  y  Icc (α - i) (α + i)) :=
λ h, sub_le_of_abs_sub_le_left h, sub_le_iff_le_add'.mp (abs_le.mp h).2⟩,
  λ h, abs_le.mpr ((sub_mem_Icc_iff α i y).mpr h)⟩

/-- An element of an open interval is closer to the left end-point than
the length of the interval. -/
lemma abs_lt_abs_left {a b c : } (hc : b  Ioo a c) :
  abs (a - b) < abs (a - c) :=
begin
  rw [abs_lt, neg_lt, lt_abs, lt_abs, neg_sub, neg_sub],
  exact or.inr (sub_lt_sub_right hc.2 a), or.inr (sub_lt_sub (lt_trans hc.1 hc.2) hc.1)⟩,
end

/-- An element of an open interval is closer to the right end-point than
the length of the interval. -/
lemma abs_lt_abs_right {a b c : } (hc : b  Ioo a c) :
  abs (c - b) < abs (a - c) :=
begin
  rw [abs_sub, sub_eq_neg_add, sub_eq_neg_add,  neg_neg b,  neg_neg a],
  exact abs_lt_abs_left neg_lt_neg_iff.mpr hc.2, neg_lt_neg_iff.mpr hc.1⟩,
end

view this post on Zulip Ruben Van de Velde (Dec 17 2020 at 19:11):

Is there any reason to use Icc (- i) i instead of an arbitrary Icc in the first lemma?

view this post on Zulip Damiano Testa (Dec 17 2020 at 19:29):

No real reason other than a lot of the arguments use "symmetric" intervals. I can definitely change this with virtually no effort!

view this post on Zulip Damiano Testa (Dec 18 2020 at 06:10):

Below are a version of the first lemma above, with arbitrary endpoints and a proof of the symmetric one as a consequence.

Is there a preference between the simp only proof and the term mode proof in sub_mem_Icc_iff?

/-- A lemma relating a compact interval and its shifts. -/
lemma sub_mem_Icc_iff (x y l m : ) : (x - y  Icc l m  x  Icc (y + l) (y + m)) :=
by simp only [le_sub_iff_add_le', sub_le_iff_le_add', iff_self, mem_Icc]
--⟨λ a, ⟨le_sub_iff_add_le'.mp a.1, sub_le_iff_le_add'.mp a.2⟩,
--    λ b, ⟨le_sub_iff_add_le'.mpr b.1, sub_le_iff_le_add'.mpr b.2⟩⟩

/-- A lemma relating a symmetric compact interval and its shifts. -/
lemma sub_mem_Icc_iff_symmetric (x y z : ) : (x - y  Icc (- z) z  x  Icc (y - z) (y + z)) :=
by rw [sub_mem_Icc_iff, tactic.ring.add_neg_eq_sub y z]

view this post on Zulip Eric Wieser (Dec 18 2020 at 09:24):

The statement of the former would seem more natural to me with the + terms on the right commuted

view this post on Zulip Damiano Testa (Dec 18 2020 at 09:25):

You mean lemma sub_mem_Icc_iff (x y l m : ℝ) : (x - y ∈ Icc l m ↔ x ∈ Icc (l + y) (m + y))?

view this post on Zulip Eric Wieser (Dec 18 2020 at 09:26):

Also I'm surprised add_neg_eq_sub is hidden away in tactic.ring as docs#tactic.ring.add_neg_eq_sub. is there a more public name?

view this post on Zulip Damiano Testa (Dec 18 2020 at 09:27):

I was also surprised by this, but I could not find it and library_search gave me... that!

view this post on Zulip Johan Commelin (Dec 18 2020 at 09:28):

sub_eq_add_neg

view this post on Zulip Eric Wieser (Dec 18 2020 at 09:36):

Reassuringly the ring one is just written in terms of that one


Last updated: May 07 2021 at 19:12 UTC