How to multiply both sides of an inequality by a positive

Stream: new members

[Lukas Krause]

How do I do this? For context, the goal is showing that

ab \leq (a ^ 2 + b ^ 2)/2.

And I've already shown

2 * a * b \leq (a ^ 2 + b ^ 2)

[Jireh Loreaux]

How about docs#le_div_iff' ?

[Luigi Massacci]

If you don't mind hitting stuff with tactics, this also works:

import Mathlib.Tactic

variable (κ : Type _) [LinearOrderedField κ] (a b : κ)

example (h : 2 * a * b ≤ (a ^ 2 + b ^ 2)) : a*b ≤ (a ^ 2 + b ^ 2)/2 := by
  nlinarith

I made some assumptions as to where a and b come from since you did not specify

[Lukas Krause]

Jireh Loreaux said:

How about docs#le_div_iff' ?

Doesn't seem to work. Getting this error:

tactic 'apply' failed, failed to unify
  ?a ≤ ?b / ?c ↔ ?c * ?a ≤ ?b
with
  a * b ≤ (a ^ 2 + b ^ 2) / 2

case left
abcde: ℝ
h₀: 2 * a * b ≤ a ^ 2 + b ^ 2
⊢ a * b ≤ (a ^ 2 + b ^ 2) / 2

Which is bizarre because to me they look like they are the same form.

@Luigi Massacci I'll try that; my bad for not giving more context, a b and c are real numbers. Though ideally I'd like to figure it out without just hitting it with a tactic.

[Lukas Krause]

Lukas Krause said:

Jireh Loreaux said:

How about docs#le_div_iff' ?

Doesn't seem to work. Getting this error:

tactic 'apply' failed, failed to unify
  ?a ≤ ?b / ?c ↔ ?c * ?a ≤ ?b
with
  a * b ≤ (a ^ 2 + b ^ 2) / 2

case left
abcde: ℝ
h₀: 2 * a * b ≤ a ^ 2 + b ^ 2
⊢ a * b ≤ (a ^ 2 + b ^ 2) / 2

Which is bizarre because to me they look like they are the same form.

Luigi Massacci I'll try that; my bad for not giving more context, a b and c are real numbers. Though ideally I'd like to figure it out without just hitting it with a tactic.

Ok, I took a look at the solutions and it looks like I need to first check that the denominator is positive via norm_num, and then I need to use rw instead of apply. I understand the first part, but the second I'm a bit confused by. Why can't I do apply, and then check that the conditions are satisfied? Why do I have to do rw?

[Luigi Massacci]

Well then nlinarith will work with reals no problem. The lemma Jireh gave you is what you need though. Just notice that it is an iff. statement, and you need the implications. You can access each direction by writing .mp/.mpr (resp .1 or .2)

[Luigi Massacci]

You don’t have to do rw, this will do what you want for example:

import Mathlib.Tactic

variable (κ : Type _) [LinearOrderedField κ] (a b : κ)

example (h : 2 * a * b ≤ (a ^ 2 + b ^ 2)) : a*b ≤ (a ^ 2 + b ^ 2)/2 := by
  apply (le_div_iff' ?_).mpr