Cancelling Denominators for Real Inequalities

Stream: new members

[Ayush Agrawal]

I am trying to prove a simple lemma:
theorem cancel_denom {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : (a / (a+b+c) ≥ b / (a+b+c)) ) : a ≥ b :=

I tried using div_le_div_iff_right, however, I am not able to provide correct arguments. Can anyone please help?

[Johan Commelin]

Can you please post a #mwe and be more specific about what you tried/what errors you gave?

[Johan Commelin]

Then we can probably give you more helpful feedback.

[Ayush Agrawal]

I tried these:
Trial 1: using div_le_div_iff_right

import data.real.basic

theorem cancel_denom {a b c : ℝ } (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : (a / (a+b+c) ≥ b / (a+b+c)) ) : a ≥ b :=
begin
      have h1 : _ ≤ _ := h,
      have h2 : b ≤ a ↔ a ≥ b,from by {simp},
      rw ← h2,
      have habc : 0 < (a + b + c), from by {linarith},
      rw (div_le_div_iff_right habc),
end

      /-
      type mismatch at application
        div_le_div_iff_right habc
      term
        habc
      has type
        0 < a + b + c : Prop
      but is expected to have type
        ?m_1 : Type ?
      state:
      a b c : ℝ,
      ha : 0 < a,
      hb : 0 < b,
      hc : 0 < c,
      h : a / (a + b + c) ≥ b / (a + b + c),
      h1 : b / (a + b + c) ≤ a / (a + b + c),
      h2 : b ≤ a ↔ a ≥ b,
      habc : 0 < a + b + c
      ⊢ b ≤ a
      -/

Trial 2: Using cancel_denoms

import data.real.basic
theorem cancel_denom2 {a b c : ℝ } (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : (a / (a+b+c) ≥ b / (a+b+c)) ) : a ≥ b :=
begin

 have habc : 0 < (a + b + c), from by {linarith},
 cancel_denoms,
end

 /-
 a b c : ℝ,
 ha : 0 < a,
 hb : 0 < b,
 hc : 0 < c,
 h : a / (a + b + c) ≥ b / (a + b + c),
 habc : 0 < a + b + c
 ⊢ b ≤ a
 -/

Trial 3: Using div_le_div_iff_right and few more arguments:

import data.real.basic
theorem cancel_denom {a b c : ℝ } (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : (a / (a+b+c) ≥ b / (a+b+c)) ) : a ≥ b :=
begin
      have h1 : _ ≤ _ := h,
      have h2 : b ≤ a ↔ a ≥ b,from by {simp},
      rw ← h2,
      have habc : 0 < (a + b + c), from by {linarith},
      rw (@div_le_div_iff_right ℝ _ _ _ b a habc),
end

/-
      failed to synthesize type class instance for
      a b c : ℝ,
      ha : 0 < a,
      hb : 0 < b,
      hc : 0 < c,
      h : a / (a + b + c) ≥ b / (a + b + c),
      h1 : b / (a + b + c) ≤ a / (a + b + c),
      h2 : b ≤ a ↔ a ≥ b,
      habc : 0 < a + b + c
      ⊢ group ℝ
      state:
      a b c : ℝ,
      ha : 0 < a,
      hb : 0 < b,
      hc : 0 < c,
      h : a / (a + b + c) ≥ b / (a + b + c),
      h1 : b / (a + b + c) ≤ a / (a + b + c),
      h2 : b ≤ a ↔ a ≥ b,
      habc : 0 < a + b + c
      ⊢ b ≤ a
      -/

[Johan Commelin]

docs#div_le_div_iff_right

[Johan Commelin]

That last trial is a good one.

[Johan Commelin]

It claims it can't find group \R. Which makes sense.

[Johan Commelin]

So it is a hint that this is not the right lemma.

[Johan Commelin]

Instead, you want docs#div_le_div_right₀

[Ayush Agrawal]

Thanks @Johan Commelin
I tried this but faced the similar issue:
Trial 4: using div_le_div_right₀

theorem cancel_denom {a b c : ℝ } (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : (a / (a+b+c) ≥ b / (a+b+c)) ) : a ≥ b :=
begin
      have h1 : _ ≤ _ := h,
      have h2 : b ≤ a ↔ a ≥ b,from by {simp},
      rw ← h2,
      have habc : (a + b + c) ≠ 0, from by {linarith},
      rw (@div_le_div_right₀ ℝ b a (a+b+c) _ habc),
end

      /-
      failed to synthesize type class instance for
      a b c : ℝ,
      ha : 0 < a,
      hb : 0 < b,
      hc : 0 < c,
      h : a / (a + b + c) ≥ b / (a + b + c),
      h1 : b / (a + b + c) ≤ a / (a + b + c),
      h2 : b ≤ a ↔ a ≥ b,
      habc : a + b + c ≠ 0
      ⊢ linear_ordered_comm_group_with_zero ℝ
      state:
      a b c : ℝ,
      ha : 0 < a,
      hb : 0 < b,
      hc : 0 < c,
      h : a / (a + b + c) ≥ b / (a + b + c),
      h1 : b / (a + b + c) ≤ a / (a + b + c),
      h2 : b ≤ a ↔ a ≥ b,
      habc : a + b + c ≠ 0
      ⊢ b ≤ a
      -/

[Yaël Dillies]

A linear_ordered_comm_group_with_zero is a group with a zero adjoined that's less than everything in the group. For example, the nonnegative reals or the nonnegative rationals. This is not the case of ℝ, however.

[Ruben Van de Velde]

Oh yeah, (a + b + c) ≠ 0 can't be enough

[Ruben Van de Velde]

docs#div_le_div_right

[Ruben Van de Velde]

import data.real.basic

theorem cancel_denom {a b c : ℝ}
  (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : (a / (a+b+c) ≥ b / (a+b+c)) ) : a ≥ b :=
begin
  rw ge_iff_le at *,
  have habc : 0 < (a + b + c),
  { linarith },
  exact (div_le_div_right habc).mp h,
end

[Yaël Dillies]

import data.real.basic
import tactic.positivity

theorem cancel_denom {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
  (h : a / (a+b+c) ≥ b / (a+b+c)) : a ≥ b :=
(div_le_div_right $ by positivity).1 h

[Ayush Agrawal]

Thanks alot @Ruben Van de Velde and @Yaël Dillies.

[Johan Commelin]

@Ayush Agrawal Whoops, my bad. Sorry for giving wrong advice.

[Yaël Dillies]

It's a bit misleading that a linear_ordered_comm_group_with_zero is a linear_ordered_comm_group with zero but not a linear ordered comm_group_with_zero :wink:

[Johan Commelin]

I guess I'm to blame for that :see_no_evil:

[Ayush Agrawal]

Johan Commelin said:

Ayush Agrawal Whoops, my bad. Sorry for giving wrong advice.

No problem at all! I got to see this aspect more clearly so thanks.

[Yaël Dillies]

Apparently, it's Kenny: #3072

[Johan Commelin]

Sure, but he ported from the perfectoid project.

[Yaël Dillies]

I guess you're to blame for that, then :see_no_evil: