## Stream: maths

### Topic: div_pos_iff_mul_pos golf

#### Kevin Buzzard (Nov 14 2018 at 21:26):

import analysis.real

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
begin
have H : 0 < y * y := mul_self_pos Hy,
split,
intro H1,
have H2 : (x * y) / (y * y) = x / y,
rw div_eq_div_iff (ne_of_gt H) Hy,
rw mul_assoc,
rw ←H2,
apply div_pos H1 H,
intro H1,
have H2 : (x / y) * (y * y) = x * y,
rw div_mul_eq_mul_div_comm,
rw mul_div_cancel _ Hy,
rw ←H2,
exact mul_pos H1 H,
end


I was surprised this wasn't already in, for preordered semimonoids with bot or whatever

#### Mario Carneiro (Nov 14 2018 at 21:28):

I'm not, that's a weird theorem

#### Kevin Buzzard (Nov 14 2018 at 21:30):

what about 0 < x * y iff (x < 0 and y < 0) or (x > 0 and y > 0)?

#### Kevin Buzzard (Nov 14 2018 at 21:30):

and similarly for 0 < x / y

#### Kenny Lau (Nov 14 2018 at 21:31):

pos_and_pos_or_neg_and_neg_of_mul_pos?

#### Kevin Buzzard (Nov 14 2018 at 21:31):

Oh, you found it?

#### Kenny Lau (Nov 14 2018 at 21:32):

I found x*y>0 implies x,y>0 or x,y<0

#### Mario Carneiro (Nov 14 2018 at 21:32):

I guess the best decomposition of it is something like

0 < x * y
↔ (0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0)
... ↔ (0 < x ∧ 0 < y⁻¹ ∨ x < 0 ∧ y⁻¹ < 0)
... ↔ 0 < x * y⁻¹
... ↔ 0 < x / y


#### Kevin Buzzard (Nov 14 2018 at 21:32):

ha ha it's in core

#### Kevin Buzzard (Nov 14 2018 at 21:32):

I think you should use pos_and_pos_or_neg_and_neg_of_mul_pos

#### Kevin Buzzard (Nov 14 2018 at 21:32):

just for the name

#### Mario Carneiro (Nov 14 2018 at 21:33):

whenever the name gets that long my eyes cross trying to read it

#### Kevin Buzzard (Nov 14 2018 at 21:33):

we should think of a more rigorous encrypted way to name lemmas

#### Kevin Buzzard (Nov 14 2018 at 21:33):

to keep them shorter

#### Mario Carneiro (Nov 14 2018 at 21:33):

have you seen metamath naming conventions? :D

#### Mario Carneiro (Nov 14 2018 at 21:34):

it would probably be called mulanor or the like

#### Reid Barton (Nov 14 2018 at 21:34):

that's a cool name

#### Kevin Buzzard (Nov 14 2018 at 21:34):

the md5sum of pos_and_pos_or_neg_and_neg_of_mul_pos is shorter, maybe we should use that

#### Mario Carneiro (Nov 14 2018 at 21:35):

probably gzip can do better

#### Kevin Buzzard (Nov 14 2018 at 21:51):

I'm not, that's a weird theorem

How would you do

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } =
{x : ℝ | x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1)} :=


? I used this along the way to clear denominators but it was still an annoying case bash

oh god

#### Kevin Buzzard (Nov 14 2018 at 21:53):

yes it's M1F sheet 3

#### Kevin Buzzard (Nov 14 2018 at 21:53):

you should have seen my proof last year!

#### Kevin Buzzard (Nov 14 2018 at 21:54):

It took me 25 lines to get to ⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1

#### Kevin Buzzard (Nov 14 2018 at 21:55):

and now the case bash is much easier

#### Kevin Buzzard (Nov 14 2018 at 21:55):

but I had to clear denominators along the way

#### Kevin Buzzard (Nov 14 2018 at 21:57):

If it's a reasonable M1F question and if you want formal proof verification systems to be taken seriously by mathematicians, this has to be relatively straightforward

#### Reid Barton (Nov 14 2018 at 21:58):

Someone want to implement a cylindrical algebraic decomposition tactic?

#### Kevin Buzzard (Nov 14 2018 at 21:59):

Is that what's necessary?

it's a case bash

#### Kevin Buzzard (Nov 14 2018 at 21:59):

Can we make it an issue or is this unreasonable?

#### Kevin Buzzard (Nov 14 2018 at 21:59):

It's a cylindrical algebraic decomposition Mario

#### Mario Carneiro (Nov 14 2018 at 21:59):

the generalization of this to more vars is CAD

#### Reid Barton (Nov 14 2018 at 22:00):

Yeah you don't really need it for one variable & rational roots.

#### Kevin Buzzard (Nov 14 2018 at 22:00):

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } = {y : ℝ | y < 0 ∨ ((1 : ℝ) / 3 < y ∧ y < 1)} you mean like this?

#### Kevin Buzzard (Nov 14 2018 at 22:01):

It's still a pain to prove that if 1/3 < x and x < 1 then 3 * x + 1 / x < 4

#### Kevin Buzzard (Nov 14 2018 at 22:01):

My reworking to ⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1 is definitely paying dividends

#### Kenny Lau (Nov 14 2018 at 22:02):

I think you should just let the IC gang prove that

#### Mario Carneiro (Nov 14 2018 at 22:02):

in general you have to figure out ordering of real algebraic numbers which is a pain

#### Mario Carneiro (Nov 14 2018 at 22:03):

and the best known algorithm is double exponential, a great improvement over the previous algorithm

#### Kenny Lau (Nov 14 2018 at 22:05):

what a pity, I was going to use it in my next gce exam

#### Kevin Buzzard (Nov 14 2018 at 22:24):

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } =
{x : ℝ | x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1)} :=
begin
ext x,
show x ≠ 0 ∧ 3 * x + 1 / x < 4 ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1,
cases classical.em (x = 0) with H0 Hn0,
{ -- junk case x = 0
rw H0,
norm_num,
},
rw (show x ≠ 0 ↔ true, by simp [Hn0]),
rw true_and,
show (3 : ℝ) * x + 1 / x < 4 ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1,
have this : (3 : ℝ) * x + 1 / x < 4 ↔ 0 < 4 - (3 * x + 1 / x)
:= (@sub_pos ℝ (by apply_instance) (4 : ℝ) ((3 : ℝ) * x + 1 / x)).symm,
rw this,
rw ←sub_sub,
rw ←mul_one (4 - 3 * x),
-- annoying rewrite
have H : 0 < (4 - 3 * x) * 1 - 1 / x ↔ 0 < (4 - 3 * x) * (x / x) - 1 / x,
rw div_self Hn0,
rw H,
rw ←mul_div_assoc,
rw ←sub_div,
rw ←mul_pos_iff_div_pos Hn0,
replace H : x * x > 0 := mul_self_pos Hn0,
rw (show ((4 - 3 * x) * x - 1) * x = (1 - x) * x * (3 * x - 1), by ring),
-- goal now
-- ⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1
cases lt_or_ge x 0 with h h1,
-- x < 0
rw (show x < 0 ↔ true, by simp [h]),
rw true_or,
rw iff_true,
apply mul_pos_of_neg_of_neg,
refine mul_neg_of_pos_of_neg _ h,
apply sub_pos_of_lt,
apply lt_trans h zero_lt_one,
apply sub_neg_of_lt,
refine lt_trans _ zero_lt_one,
apply mul_neg_of_pos_of_neg _ h,
norm_num,
rw (show x < 0 ↔ false, by rw iff_false; exact not_lt_of_ge h1),
rw false_or,
cases le_or_gt x ((1 : ℝ) / 3) with h2 h2,
rw (show (1 : ℝ) / 3 < x ↔ false, by rw iff_false; exact not_lt_of_ge h2),
rw false_and,
rw iff_false,
apply not_lt_of_ge,
refine mul_nonpos_of_nonneg_of_nonpos _ _,
refine mul_nonneg _ h1,
show 0 ≤ 1 - x,
rw sub_nonneg,
exact le_trans h2 (by norm_num),
rw sub_nonpos,
rw mul_comm,
apply mul_le_of_le_div (by norm_num) h2,
cases lt_or_ge x 1,
rw (iff_true ((1 : ℝ) / 3 < x)).2 h2,
rw (iff_true (x < 1)).2 h,
rw true_and,
rw iff_true,
refine mul_pos _ _,
refine mul_pos _ _,
show 0 < (1 - x),
rwa sub_pos,
refine lt_trans (by norm_num) h2,
show 0 < 3 * x - 1,
rw sub_pos,
rwa ←div_lt_iff',
norm_num,
rw (show x < 1 ↔ false, by rw iff_false; exact not_lt_of_ge h),
rw and_false,
rw iff_false,
apply not_lt_of_ge,
refine mul_nonpos_of_nonpos_of_nonneg _ _,
refine mul_nonpos_of_nonpos_of_nonneg _ h1,
simp [h], exact h,
show 0 ≤ 3 * x - 1,
rw sub_nonneg,
rw mul_comm,
apply le_mul_of_div_le,
norm_num,
apply le_trans _ h,
norm_num,
end


Much better than last year's effort

"much better"

thanks

#### Kenny Lau (Nov 14 2018 at 23:02):

import analysis.real

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } =
{x : ℝ | x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1)} :=
begin
ext x,
rcases lt_trichotomy x 0 with hxneg | hx0 | hxpos,
{ refine iff_of_true ⟨ne_of_lt hxneg, _⟩ (or.inl hxneg),
refine lt_trans (add_neg (mul_neg_of_pos_of_neg _ hxneg) (one_div_neg_of_neg hxneg)) _;
norm_num },
{ subst x, norm_num },
show x ≠ 0 ∧ 3 * x + 1 / x < 4 ↔ x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1),
rw [eq_true_intro (ne_of_gt hxpos)],
rw [true_and],
rw [eq_false_intro (not_lt_of_gt hxpos)],
rw [false_or],
rw [← mul_lt_mul_right hxpos],
rw [one_div_mul_cancel (ne_of_gt hxpos)],
rw [div_lt_iff (show (0:ℝ) < 3, by norm_num)],
split,
{ assume h : 3 * x * x + 1 < 4 * x,
replace h := sub_neg_of_lt h,
rw [show 3 * x * x + 1 - 4 * x = (1 - x * 3) * (1 - x), by ring] at h,
have : 1 < x * 3,
{ apply lt_of_not_ge,
assume h2 : x * 3 ≤ 1,
replace h := neg_of_mul_neg_left h (sub_nonneg_of_le h2),
refine not_lt_of_le h2 _,
refine lt_trans (show (1:ℝ) < 3, by norm_num) _,
replace h := lt_of_sub_neg h,
rw [← mul_lt_mul_right (show (0:ℝ) < 3, by norm_num)] at h,
rwa [one_mul] at h },
refine ⟨this, lt_of_sub_pos _⟩,
apply lt_of_not_ge,
assume h3 : 1 - x ≤ 0,
apply not_le_of_lt h,
exact mul_nonneg_of_nonpos_of_nonpos (le_of_lt (sub_neg_of_lt this)) h3 },
{ assume h : 1 < x * 3 ∧ x < 1,
cases h with h1 h2,
apply lt_of_sub_neg,
rw [show 3 * x * x + 1 - 4 * x = (1 - x * 3) * (1 - x), by ring],
exact mul_neg_of_neg_of_pos (sub_neg_of_lt h1) (sub_pos_of_lt h2) }
end


@Kevin Buzzard

#### Kevin Buzzard (Nov 14 2018 at 23:04):

It's still a lot longer than what most of the first years produce with pen and paper though isn't it :-/

#### Kevin Buzzard (Nov 14 2018 at 23:06):

you did the case split at the start. I worked on the goal first. Is your way better or would you have written half as much as me if you'd used my strategy too?

#### Kenny Lau (Nov 14 2018 at 23:06):

btw:

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
begin
have := mul_self_pos Hy,
rw ← @mul_lt_mul_right _ _ _ (x/y) _ this,
rw zero_mul,
rw ← mul_assoc,
rw div_mul_cancel _ Hy
end


#### Kenny Lau (Nov 14 2018 at 23:07):

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
by rw [← @mul_lt_mul_right _ _ _ (x/y) _ (mul_self_pos Hy)];
rw [zero_mul, ← mul_assoc, div_mul_cancel _ Hy]


#### Kenny Lau (Nov 14 2018 at 23:09):

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
by rw [← div_lt_div_right (mul_self_pos Hy), zero_div, ← div_div_eq_div_mul, mul_div_cancel _ Hy]


(98 characters!)

#### Kenny Lau (Nov 14 2018 at 23:10):

you did the case split at the start. I worked on the goal first. Is your way better or would you have written half as much as me if you'd used my strategy too?

I mean, you also did case split at the start

#### Reid Barton (Nov 14 2018 at 23:11):

Isn't that Hy hypothesis actually unneeded?

#### Reid Barton (Nov 14 2018 at 23:11):

If y = 0 then both things are 0

great

#### Kenny Lau (Nov 14 2018 at 23:14):

"Lean helps me understand maths better"

#### Kenny Lau (Nov 14 2018 at 23:15):

"y doesn't need to be nonzero"

#### Mario Carneiro (Nov 15 2018 at 01:40):

import data.real.basic tactic.ring data.set.intervals

theorem mul_pos_iff {α} [linear_ordered_ring α] {a b : α} :
0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
⟨pos_and_pos_or_neg_and_neg_of_mul_pos,
or.rec (and.rec mul_pos) (and.rec \$ by exact mul_pos_of_neg_of_neg)⟩

theorem or_iff_left {a b : Prop} (h : ¬ b) : a ∨ b ↔ a :=
or_iff_left_of_imp h.elim

theorem or_iff_right {a b : Prop} (h : ¬ a) : a ∨ b ↔ b :=
or_iff_right_of_imp h.elim

open set
theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } = Iio 0 ∪ Ioo (1 / 3) 1 :=
begin
ext x,
rcases lt_trichotomy x 0 with x0|x0|x0,
{ refine iff_of_true ⟨ne_of_lt x0,
(mul_neg_of_pos_of_neg _ x0)
(one_div_neg_of_neg x0)) _⟩ (or.inl x0);
norm_num },
{ subst x, norm_num },
{ dsimp [Iio, Ioo],
rw [and_iff_right (ne_of_gt x0), or_iff_right (not_lt_of_gt x0),
div_lt_iff x0, div_lt_iff' (by norm_num : 0 < (3:ℝ)), ← sub_pos,
(by ring : 4*x - (3*x*x + 1) = (3*x - 1)*(1 - x)),
mul_pos_iff, sub_pos, sub_pos, sub_lt_zero, sub_lt_zero,
or_iff_left],
rintro ⟨h₁, h₂⟩,
refine absurd (lt_trans h₂ ((lt_div_iff' _).2 h₁)) _; norm_num }
end


#### Kevin Buzzard (Nov 15 2018 at 02:55):

I shall explode this proof tomorrow

#### Patrick Massot (Nov 15 2018 at 08:37):

Mario, why do you need to explicitly invoke all those and_iff_right, or_iff_right, or_iff_left? Isn't it something that the simplifier should do (using hypothesis x0)?

#### Patrick Massot (Nov 15 2018 at 08:43):

Makes me think: @Simon Hudon what happened to your monotonicity tactic?

#### Simon Hudon (Nov 15 2018 at 16:39):

Mario is still unhappy with it.

Last updated: May 10 2021 at 07:15 UTC