Halving inequaities

Stream: maths

[Jakob von Raumer]

Am I wrong or are the following inequalities missing?

lemma nat.le_half_of_le_of_half_lt_sub {a b : ℕ} (h : a / 2 < a - b) : b ≤ a / 2

and

lemma nat.ge_half_of_sub_le_half {a b : ℕ} (h : a - b ≤ a / 2) : b ≥ a / 2

[Riccardo Brasca]

Do you really want to use / and - for natural numbers?

[Riccardo Brasca]

I mean, I don't even know if these are true (too lazy to check :grinning_face_with_smiling_eyes: )

[Jakob von Raumer]

"want" is a bit of a stretch but I have to :sweat_smile:

[Kevin Buzzard]

What does slim_check think about them?

[Kevin Buzzard]

By the way, no ge lemmas should be in mathlib, always write inequalities as le.

[Kyle Miller]

I was incidentally just checking it with slim_check

[Kyle Miller]

they seem to be ok

[Kyle Miller]

Here's the first one:

lemma nat.le_half_of_half_lt_sub {a b : ℕ} (h : a / 2 < a - b) : b ≤ a / 2 :=
begin
  rw nat.le_div_iff_mul_le two_pos,
  rw [nat.div_lt_iff_lt_mul two_pos, nat.mul_sub_right_distrib, lt_tsub_iff_right] at h,
  linarith,
end

[Kyle Miller]

and the second:

lemma nat.half_le_of_sub_le_half {a b : ℕ} (h : a - b ≤ a / 2) : a / 2 ≤ b :=
begin
  rw [nat.le_div_iff_mul_le two_pos, nat.mul_sub_right_distrib, tsub_le_iff_right,
    mul_two, add_le_add_iff_left] at h,
  rw [← nat.mul_div_left b two_pos],
  exact nat.div_le_div_right h,
end

[Alex J. Best]

I miss omega...

[Kevin Buzzard]

Why not write it in Lean 4 Alex!

[Jakob von Raumer]

@Kyle Miller Oh wow, thats much shorter than my solution

[Jakob von Raumer]

@Alex J. Best What's omega?

[Yaël Dillies]

tactic#omega

[Jakob von Raumer]

... and is it broken?

[Kevin Buzzard]

It got banned from mathlib, for unreasonable behaviour.

[Ruben Van de Velde]

I thought mostly for it not being maintained and probably not ported to lean4 any time soon, but maybe both :)

[Jakob von Raumer]

@Kyle Miller Is it okay if I PR those lemmas together with

lemma zmod.val_min_abs_neg_of_ne_half {n : ℕ} {a : zmod n} (ha : a.val ≠ n / 2) :
  (-a).val_min_abs = -a.val_min_abs :=
begin
  cases n, refl,
  simp only [zmod.val_min_abs_def_pos, zmod.neg_val],
  split_ifs with h h' h'' h'' h' h'' h'';
    try { subst h, simp only [zmod.nat_cast_self, nat.cast_succ, zero_sub, neg_add_rev,
       zmod.val_zero, neg_zero', neg_neg, zero_le', not_true, ne.def] at *}; try { contradiction },
  { exfalso, apply not_le.mpr (lt_of_le_of_ne h'' ha) (nat.half_le_of_sub_le_half h') },
  { rw [neg_sub, nat.cast_sub], apply le_of_lt (zmod.val_lt a) },
  { rw [nat.cast_sub (le_of_lt (zmod.val_lt a))], simp only [sub_sub_cancel_left] },
  { exfalso, clear ha,
    rw [not_le] at h',
    exact h'' (nat.le_half_of_half_lt_sub h') }
end

[Jakob von Raumer]

We weirdly only have zmod.nat_abs_val_min_abs_neg right now

[Jakob von Raumer]

Ah I guess the whole definition is tailored to the Eisenstein lemmas

[Kyle Miller]

@Jakob von Raumer Feel free to take the two lemmas as your own! They seem potentially useful to have around.