a problem of reduction in lean4

Stream: maths

[Junqi Liu]

how to solve $x * (1 - x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - x) * √(x * z) * 2 * √(1 - y) * √((1 - z) * y)) ≤ √x * √(1 - x) * √y * √(1 - y) * √z * √(1 - z) / 4$ for $x, y, z \in (0,1)$ in lean4?

[Riccardo Brasca]

Can you explain the math proof?

[Jireh Loreaux]

Aren't those two sides just equal?

[Riccardo Brasca]

Ahah, yes, it seems they're equal!

[Junqi Liu]

Jireh Loreaux said:

Aren't those two sides just equal?

yeah. But that doesn't affect the proof, does it?

[Junqi Liu]

Jireh Loreaux said:

Aren't those two sides just equal?

This is just a step to divide the numerator and the denominator.

[Jireh Loreaux]

ahhwuhu said:

yeah. But that doesn't affect the proof, does it?

sure it does. You can apply more lemmas / tactics with equality.

[Jireh Loreaux]

In the hope that automation would make my life easy, I would rewrite the numerator of the left-hand side into a bunch of square roots, use positivity to conclude they are all nonzero, and then use field_simp and pray.

[Junqi Liu]

oh! You're absolutely right! But I want to know why the simp command doesn't work?

[Jireh Loreaux]

what do you mean? what do you expect simp to do exactly?

[Junqi Liu]

Can simp not be divided directly?

[Jireh Loreaux]

I'm not sure what you mean.

[Junqi Liu]

emmmmmm. I mean, like $\frac{x^2}{x} = x$, can I successfully prove it directly using simp command?

[Andrew Yang]

This is false in mathlib for x = 0.

[Andrew Yang]

So simp won't work directly. Maybe if you give it a h : x =/= 0 then simp [h] will work.

[Junqi Liu]

sure! But if $x \in (0,1)$, does it ok?

[Riccardo Brasca]

Yes, if x is different from 0 then this is true, but the point is that division in Lean is trickier than one usually thinks

[Riccardo Brasca]

field_simp is supposed to help, but you need to give it the fact that the denominator is different from 0.

[Junqi Liu]

Riccardo Brasca said:

Yes, if x is different from 0 then this is true, but the point is that division in Lean is trickier than one usually thinks

Thanks! I feel that. Let me have a try!

[Andrew Yang]

For example this works

import Mathlib

example {x : ℝ} (hx : x ≠ 0) : (x * x) / x = x := by simp [hx]

But you'll need to let simp know about x ≠ 0 manually.

[Yaël Dillies]

Andrew Yang said:

This is false in mathlib for x = 0.

Actually it is true!

[Jireh Loreaux]

Here's a proof:

example (x y z : ℝ) (hx : 0 < x) (hx' : 0 < 1 - x) (hy : 0 < y) (hy' : 0 < 1 - y) (hz : 0 < z) (hz' : 0 < 1 - z) :
    x * (1 - x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - x) * √(x * z) * 2 * √(1 - y) * √((1 - z) * y)) =
      √x * √(1 - x) * √y * √(1 - y) * √z * √(1 - z) / 4 := by
  field_simp
  nth_rewrite 1 [← Real.mul_self_sqrt hx.le, ← Real.mul_self_sqrt hy.le, ← Real.mul_self_sqrt hz.le]
  conv_lhs =>
    rw [← Real.mul_self_sqrt hx'.le, ← Real.mul_self_sqrt hy'.le, ← Real.mul_self_sqrt hz'.le]
  ring

[Andrew Yang]

Oh I thought 0/0 = 1...

[Junqi Liu]

example (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z0 : 0 < z) (z1 : z < 1) : x * (1 - x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - x) * √(x * z) * 2 * √(1 - y) * √((1 - z) * y)) =
  √x * √(1 - x) * √y * √(1 - y) * √z * √(1 - z) / 4

Can anyone help me solve it?

[Jireh Loreaux]

@ahhwuhu see my post just above.

[Junqi Liu]

Jireh Loreaux said:

just

Very thanks! Let me see!

[Junqi Liu]

And I have another question. Is there any difference between my use of $\sqrt{x}$ and Real.sqrt x?

[Jireh Loreaux]

no, they're the same.

[Junqi Liu]

okk! Thanks a lot!