If `a + b ≤ 2 * c` then one of them is `≤ c`

Stream: Is there code for X?

[Eric Wieser]

Do we have anything resembling the following?

import data.nat.order.lemmas
import tactic.linarith

lemma min_le_of_add_le_two_mul {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  (a b c : α) (h : a + b ≤ 2 * c) : min a b ≤ c :=
begin
  cases le_total a b with hab hba,
  { refine (min_le_left _ _).trans _,
    obtain ⟨b, rfl⟩ := exists_add_of_le hab,
    have := (add_le_add_left hab a).trans h,
    rw ←two_mul at this,
    exact le_of_mul_le_mul_left this zero_lt_two },
  { refine (min_le_right _ _).trans _,
    obtain ⟨a, rfl⟩ := exists_add_of_le hba,
    have := (add_le_add_right hba b).trans h,
    rw ←two_mul at this,
    exact le_of_mul_le_mul_left this zero_lt_two },
end

Is this the correct set of typeclasses? Or can it be made to work with smul instead of mul?

cc @Junyan Xu (the context is #17743) and @Yaël Dillies (this is order stuff)

[Yaël Dillies]

It reminds me of docs#add_le_add_iff_of_ge

[Yaël Dillies]

Probably the correct thing to prove is

@[to_additive]
lemma min_le_max_of_mul_le_mul [not_sure α] [has_exists_mul_of_le α]
  {a b c d : α} (h : a * b ≤ c * d) : min a b ≤ max c d := sorry

[Eric Wieser]

Obviously the follow-up is the n-ary versions

[Yaël Dillies]

I think the key property you want is a ^ 2 ≤ b ^ 2 → a ≤ b. Then the proof is (min a b) ^ 2 ≤ a * b ≤ c * d ≤ (max c d) ^ 2.

[Eric Wieser]

Indeed, if I prove (h : a + b ≤ c + d) : min a b ≤ max c d first them my lemmas falls out as special cases

[Eric Wieser]

lemma le_of_two_nsmul_le_two_nsmul {α} [linear_ordered_semiring α]
  {a b : α} (h : 2 • a ≤ 2 • b) : a ≤ b :=
begin
  rw [two_nsmul, two_nsmul, ←two_mul, ←two_mul] at h,
  exact le_of_mul_le_mul_left h zero_lt_two
end

lemma min_le_max_of_add_le_add {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  {a b c d : α} (h : a + b ≤ c + d) : min a b ≤ max c d :=
begin
  cases le_total a b with hab hba,
  { refine (min_le_left _ _).trans _,
    obtain ⟨b, rfl⟩ := exists_add_of_le hab,
    cases le_total c d with hcd hdc,
    { refine le_trans _ (le_max_right _ _),
      obtain ⟨d, rfl⟩ := exists_add_of_le hcd,
      have := ((add_le_add_left hab _).trans h).trans (add_le_add_right hcd _),
      rw [←two_nsmul, ←two_nsmul] at this,
      exact le_of_two_nsmul_le_two_nsmul this },
    { refine le_trans _ (le_max_left _ _),
      obtain ⟨c, rfl⟩ := exists_add_of_le hdc,
      have := ((add_le_add_left hab _).trans h).trans (add_le_add_left hdc _),
      rw [←two_nsmul, ←two_nsmul] at this,
      exact le_of_two_nsmul_le_two_nsmul this } },
  { refine (min_le_right _ _).trans _,
    obtain ⟨a, rfl⟩ := exists_add_of_le hba,
    cases le_total c d with hcd hdc,
    { refine le_trans _ (le_max_right _ _),
      obtain ⟨d, rfl⟩ := exists_add_of_le hcd,
      have := ((add_le_add_right hba _).trans h).trans (add_le_add_right hcd _),
      rw [←two_nsmul, ←two_nsmul] at this,
      exact le_of_two_nsmul_le_two_nsmul this },
    { refine le_trans _ (le_max_left _ _),
      obtain ⟨c, rfl⟩ := exists_add_of_le hdc,
      have := ((add_le_add_right hba _).trans h).trans (add_le_add_left hdc _),
      rw [←two_nsmul, ←two_nsmul] at this,
      exact le_of_two_nsmul_le_two_nsmul this } },
end

lemma min_le_of_add_le_two_mul {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  {a b c : α} (h : a + b ≤ 2 * c) : min a b ≤ c :=
by simpa using min_le_max_of_add_le_add (h.trans_eq $ two_mul _)

lemma le_max_of_add_le_two_mul {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  {a b c : α} (h : 2 * c ≤ a + b) : c ≤ max a b :=
by simpa using min_le_max_of_add_le_add ((two_mul _).symm.trans_le h)

[Yaël Dillies]

Can you first prove a ^ 2 ≤ b ^ 2 → a ≤ b as I suggested above?

[Eric Wieser]

I doubt it, I expect we don't have any proof that can be additivized here without some new typeclasses

[Yaël Dillies]

We sure do. linear_order + monotonicity of multiplication is already enough.

[Yaël Dillies]

Something like docs#le_of_pow_le_pow (which is definitely a misnomer!)

[Yaël Dillies]

And of course you can generalise this to any strictly monotone function. So the real deal is docs#strict_mono.reflect_le. We only have docs#monotone.reflect_lt :sad: .

[Eric Wieser]

Edited the above to at least extract the lemma you asked for

[Yaël Dillies]

/me is writing a new proof

[Kevin Buzzard]

These look easy by contradiction

[Kevin Buzzard]

lemma min_le_of_add_le_two_mul {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  (a b c : α) (h : a + b ≤ 2 * c) : min a b ≤ c :=
begin
  refine le_imp_le_of_lt_imp_lt (λ h2, _) h,
  cases lt_min_iff.1 h2 with h3 h4,
  rw two_mul,
  exact add_lt_add h3 h4,
end

lemma le_max_of_add_le_two_mul {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  (a b c : α) (h : 2 * c ≤ a + b) : c ≤ max a b :=
begin
  refine le_imp_le_of_lt_imp_lt (λ h2, _) h,
  cases max_lt_iff.1 h2 with h3 h4,
  rw two_mul,
  exact add_lt_add h3 h4,
end

[Kevin Buzzard]

import data.nat.order.lemmas
import tactic.linarith

lemma min_le_max_of_add_le_add {α} [linear_ordered_semiring α] [has_exists_add_of_le α]
  {a b c d : α} (h : a + b ≤ c + d) : min a b ≤ max c d :=
begin
  refine le_imp_le_of_lt_imp_lt (λ h2, _) h,
  rw [max_lt_iff, lt_min_iff, lt_min_iff] at h2,
  rcases h2 with ⟨⟨h3, -⟩, ⟨-, h4⟩⟩,
  exact add_lt_add h3 h4,
end

[Kevin Buzzard]

Proving a conclusion min a b <= c is annoying because you don't know which one will be the min. But having a hypothesis c < min a b is really powerful because you can deduce c < a and c < b.

[Yaël Dillies]

import algebra.group_power.basic
import algebra.order.monoid.lemmas
import order.lattice

open function

variables {α β : Type*}

section preorder
variables [add_monoid α] [preorder α] [preorder β] {f g : β → α}
  [covariant_class α α (+) (<)] [covariant_class α α (swap (+)) (<)]

lemma strict_mono.nsmul (hf : strict_mono f) : ∀ {n : ℕ}, n ≠ 0 → strict_mono (λ a, n • f a)
| 0 hn := (hn rfl).elim
| 1 hn := by simpa
| (n + 2) hn := by { simp_rw succ_nsmul _ (n + 1), exact hf.add (strict_mono.nsmul n.succ_ne_zero) }

end preorder

section preorder
variables [monoid α] [preorder α] [preorder β] {f g : β → α}
  [covariant_class α α (*) (<)] [covariant_class α α (swap (*)) (<)]

@[to_additive]
lemma strict_mono.pow (hf : strict_mono f) : ∀ {n : ℕ}, n ≠ 0 → strict_mono (λ a, f a ^ n)
| 0 hn := (hn rfl).elim
| 1 hn := by simpa
| (n + 2) hn := by { simp_rw pow_succ _ (n + 1), exact hf.mul' (strict_mono.pow n.succ_ne_zero) }

@[to_additive]
lemma strict_mono_pow {n : ℕ} (hn : n ≠ 0) : strict_mono (λ a : α, a ^ n) := strict_mono_id.pow hn

end preorder

section linear_order
variables [monoid α] [linear_order α] [covariant_class α α (*) (<)]
  [covariant_class α α (swap (*)) (<)] {a b c d : α} {n : ℕ}

@[to_additive le_of_nsmul_le_nsmul]
lemma le_of_pow_le_pow' {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b :=
(strict_mono_pow hn).le_iff_le.1

variables [covariant_class α α (*) (≤)] [covariant_class α α (swap (*)) (≤)]

@[to_additive]
lemma min_le_max_of_mul_le_mul (h : a * b ≤ c * d) : min a b ≤ max c d :=
le_of_pow_le_pow' two_ne_zero $ by { simp_rw pow_two, exact (mul_le_mul' inf_le_left
  inf_le_right).trans (h.trans $ mul_le_mul' le_sup_left le_sup_right) }

end linear_order

[Yaël Dillies]

This all follows what I said above.

[Yaël Dillies]

(btw I'm a bit horrified by the amount of imports I need to say "give me basic algebraic order theory". How come lattices not be imported by the algebraic order hierarchy?)

[Junyan Xu]

Kevin's proof also works under these assumptions (don't even need to assume [covariant_class α α (*) (≤)] [covariant_class α α (swap (*)) (≤)]:

import algebra.order.monoid.defs
import order.min_max

lemma min_le_max_of_add_le_add {α} [has_add α] [linear_order α]
  [covariant_class α α (+) (<)] [covariant_class α α (function.swap (+)) (<)]
  (a b c d : α) (h : a + b ≤ c + d) : min a b ≤ max c d :=
begin
  simp_rw [min_le_iff, le_max_iff],
  contrapose! h,
  exact add_lt_add h.1.1 h.2.2,
end

[Eric Wieser]

Are the lt versions easy too, with either spelling?

[Eric Wieser]

Note that docs#zpow_strict_mono already exists, so your name might need disambiguating somehow

[Junyan Xu]

It's worrying that docs#zpow_strict_mono_left and docs#pow_strict_mono_left aren't analogous facts ...

[Yaël Dillies]

I've been annoyed for a long at those names but it's really hard to come up with better names before you have all the lemmas.

[Junyan Xu]

Are the lt versions easy too, with either spelling?

If you mean this, it holds with (<) in the covariant hypotheses replaced by (≤), or under the cleaner assumption linear_ordered_add_comm_monoid:

lemma min_lt_max_of_add_lt_add {α} [linear_ordered_add_comm_monoid α]
  (a b c d : α) (h : a + b < c + d) : min a b < max c d :=
begin
  simp_rw [min_lt_iff, lt_max_iff],
  contrapose! h,
  exact add_le_add h.1.1 h.2.2,
end

[Junyan Xu]

(I think the (≤) version doesn't necessarily hold for linear_ordered_add_comm_monoid because you can consider absorptive addition on {0,1,2} then you'd have 1 + 1 = 2 + 2 = 2 but 2 ≰ 1.)

[Yaël Dillies]

Updated my snippet above to include the < versions.

[Eric Wieser]

Is the mathlib4 tide past the natural place to PR these yet?

[Yaël Dillies]

Mostly not, but it's very close to the border.

[Eric Wieser]

Are you happy to PR the earlier mono lemmas?

[Eric Wieser]

#17895