intervals, abs and shifts

Stream: Is there code for X?

[Damiano Testa]

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

[Ruben Van de Velde]

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

[Damiano Testa]

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

[Damiano Testa]

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]

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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?

[Damiano Testa]

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

[Johan Commelin]

sub_eq_add_neg

[Eric Wieser]

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