## Stream: new members

### Topic: Match lhs and rhs of inequality

#### Kunhao Zheng (Jun 10 2021 at 09:17):

Hello! Currently I am trying to formalizing some inequality exercises involving amgm. Here is the first draft that works.

import data.real.basic
import analysis.mean_inequalities
import analysis.special_functions.pow

theorem algebra_amgm2_a2oncpc2onbpb2onaleqa3conb3pb3aonc3pc3bona3
(a b c : ℝ)
(h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
a^2 / c + c^2 / b + b^2 / a ≤ a^3 * c / b^3 + b^3 * a / c^3 + c^3 * b / a^3 :=
begin
have ha₃ := pow_pos h₀.1 3,
have hb₃ := pow_pos h₀.2.1 3,
have hc₃ := pow_pos h₀.2.2 3,
have h₁ := le_of_lt (div_pos (mul_pos hb₃ h₀.1) hc₃),
have h₂ := le_of_lt (div_pos (mul_pos hc₃ h₀.2.1) ha₃),
have h₃ := le_of_lt (div_pos (mul_pos ha₃ h₀.2.2) hb₃),
have h₄ : (0:ℝ) ≤ 1 / 2, norm_num,
have h₅ : 1 / 2 + 1 / 2 = (1:ℝ), ring,
have h₆ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₂ h₅,
have h₇ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₃ h₅,
have h₈ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₂ h₃ h₅,
clear h₆ h₇ h₈,
have lhs : (b^3 * a / c^3)^((1:ℝ) / 2) * (a^3 * c / b^3)^((1:ℝ) / 2) +
(c^3 * b / a^3)^((1:ℝ) / 2) * (a^3 * c / b^3)^((1:ℝ) / 2) +
(b^3 * a / c^3)^((1:ℝ) / 2) * (c^3 * b / a^3)^((1:ℝ) / 2) =
a^2 / c + c^2 / b + b^2 / a, {
simp only [←real.mul_rpow, h₁, h₂, h₃],
{
have pow_can₁: a^2 / c = ((a^2 / c) ^ ((2:ℕ):ℝ)) ^ ((1:ℝ) / 2), {
simp [←real.rpow_mul, le_of_lt (div_pos (pow_pos h₀.1 2) h₀.2.2)],
},
rw pow_can₁,
refine congr_fun (congr_arg pow _) _,
rw [real.rpow_nat_cast],
field_simp [ne_of_gt hb₃, ne_of_gt hc₃, pow_succ' c 2, ne_of_gt h₀.2.2, mul_div_cancel_left],
ring_nf,
},
{
have pow_can₂: c^2 / b = ((c^2 / b) ^ ((2:ℕ):ℝ)) ^ ((1:ℝ) / 2), {
simp [←real.rpow_mul, le_of_lt (div_pos (pow_pos h₀.2.2 2) h₀.2.1)],
},
rw pow_can₂,
refine congr_fun (congr_arg pow _) _,
rw [real.rpow_nat_cast],
field_simp [ne_of_gt ha₃, ne_of_gt hb₃, pow_succ' b 2, ne_of_gt h₀.2.1, mul_div_cancel_left],
ring_nf,
},
{
have pow_can₃: b^2 / a = ((b^2 / a) ^ ((2:ℕ):ℝ)) ^ ((1:ℝ) / 2), {
simp [←real.rpow_mul, le_of_lt (div_pos (pow_pos h₀.2.1 2) h₀.1)],
},
rw pow_can₃,
refine congr_fun (congr_arg pow _) _,
rw [real.rpow_nat_cast],
field_simp [ne_of_gt hc₃, ne_of_gt hb₃, pow_succ' a 2, ne_of_gt h₀.1, mul_div_cancel_left],
ring_nf,
},
},
have rhs : 1 / 2 * (b^3 * a / c^3) + 1 / 2 * (a^3 * c / b^3) +
(1 / 2 * (c^3 * b / a^3) + 1 / 2 * (a^3 * c / b^3)) +
(1 / 2 * (b^3 * a / c^3) + 1 / 2 * (c^3 * b / a^3)) =
a^3 * c / b^3 + b^3 * a / c^3 + c^3 * b / a^3, {
ring_nf,
},
rwa [←lhs, ←rhs],
end


The roadmap is to construct an inequality forwardly (h₉) then prove its lhs and rhs can simplify to the goal's. I have to state explicitly the lhs and rhs here because I didn't find any tactic that helps with this kind of situation, something like

import data.real.basic

lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d :=
begin
sorry
end


can help me use the refine tactic to generate 2 subgoals of equalities. But I can only find tactic for 1 equality like eq.trans_le. Also, my proof is very forward reasony so I wonder if you have any advice on the proof itself.

#### Sebastien Gouezel (Jun 10 2021 at 09:25):

import data.real.basic

lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d :=
begin
linarith,
end


#### Eric Wieser (Jun 10 2021 at 11:07):

Do we have docs#has_le.le.trans_eq?

#### Eric Wieser (Jun 10 2021 at 11:08):

j.symm.le.trans (h.trans k.le) is a short term-mode proof

#### Johan Commelin (Jun 10 2021 at 11:14):

j.symm.le is j.ge

#### Johan Commelin (Jun 10 2021 at 11:14):

But I guess we don't get a trans then?

#### Johan Commelin (Jun 10 2021 at 11:16):

Of course by rwa [j, k] at h also works

#### Damiano Testa (Jun 10 2021 at 11:17):

I find that what is below is closer to how I think of it:

import data.real.basic

lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d :=
begin
convert h,  --  I know the correct inequality is this one
{ exact j.symm },  -- now fix it!
{ exact k.symm }
end


#### Damiano Testa (Jun 10 2021 at 11:19):

For increased opacity, this also works:

by convert h; exact eq.symm ‹_›


#### Damiano Testa (Jun 10 2021 at 11:20):

Although, while the term mode proofs that have been given earlier are probably closer to mathlib proofs (and also how I would write them), using convert is often more "mathematical".

#### Damiano Testa (Jun 10 2021 at 11:22):

In particular, my impression is that the role of h is fundamental, while the extra equalities are noise. Beginning a proof with convert h is bringing the attention to what matters. After that, what is left is figuring out that you do indeed have the pieces of the puzzle.

#### Eric Wieser (Jun 10 2021 at 11:36):

You can also use the equation compiler for this type of thing:

import data.real.basic

lemma trans_le_trans : ∀
(a b c d : ℝ)
(j : a = c)
(k : b = d)
(h : a ≤ b),
c ≤ d
| _ _ _ _ rfl rfl h := h


#### Eric Wieser (Jun 10 2021 at 11:37):

But tactic#linarith is the best "I don't care about this stuff just solve it for me" solution.

#### Kunhao Zheng (Jun 10 2021 at 11:40):

Eric Wieser said:

You can also use the equation compiler for this type of thing:

import data.real.basic

lemma trans_le_trans : ∀
(a b c d : ℝ)
(j : a = c)
(k : b = d)
(h : a ≤ b),
c ≤ d
| _ _ _ _ rfl rfl h := h


could you please explain more about this syntax? I don't quite understand what's going on here (especially the | and the , after (h : a ≤ b))

#### Johan Commelin (Jun 10 2021 at 11:41):

@Kunhao Zheng Note that the is now a \forall on the first line of the lemma

#### Johan Commelin (Jun 10 2021 at 11:41):

So the , is just \forall bla, blabla

#### Yakov Pechersky (Jun 10 2021 at 11:46):

Also possible term mode is to use eq.subst, I think (k.subst (j.subst h)) will work. The rw triangle.

#### Yakov Pechersky (Jun 10 2021 at 11:49):

Regarding the proof and reverse reasoning, untested, but after you prove that the cubes are nonnegative, can you try field_simp? That should multiply everything out

#### Kunhao Zheng (Jun 10 2021 at 12:00):

Yakov Pechersky said:

Regarding the proof and reverse reasoning, untested, but after you prove that the cubes are nonnegative, can you try field_simp? That should multiply everything out

Now my proof looks like this:

import data.real.basic
import analysis.mean_inequalities
import analysis.special_functions.pow

lemma trans_le_trans
{a b c d : ℝ}
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d := k.subst(j.subst h)

lemma pow_two_pow_half
(a : ℝ)
(h : 0 < a) :
a = (a^2)^((1:ℝ) / 2) :=
begin
simp [←real.rpow_mul, le_of_lt h, ←real.rpow_nat_cast],
end

theorem algebra_amgm2_a2oncpc2onbpb2onaleqa3conb3pb3aonc3pc3bona3
(a b c : ℝ)
(h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
a^2 / c + c^2 / b + b^2 / a ≤ a^3 * c / b^3 + b^3 * a / c^3 + c^3 * b / a^3 :=
begin
have ha₃ := pow_pos h₀.1 3,
have hb₃ := pow_pos h₀.2.1 3,
have hc₃ := pow_pos h₀.2.2 3,
have h₁ := le_of_lt (div_pos (mul_pos hb₃ h₀.1) hc₃),
have h₂ := le_of_lt (div_pos (mul_pos hc₃ h₀.2.1) ha₃),
have h₃ := le_of_lt (div_pos (mul_pos ha₃ h₀.2.2) hb₃),
have h₄ : (0:ℝ) ≤ 1 / 2, norm_num,
have h₅ : 1 / 2 + 1 / 2 = (1:ℝ), ring,
have h₆ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₂ h₅,
have h₇ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₃ h₅,
have h₈ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₂ h₃ h₅,
clear h₆ h₇ h₈,
refine trans_le_trans h₉ _ _,
{
simp only [←real.mul_rpow, h₁, h₂, h₃],
rw [pow_two_pow_half (a ^ 2 / c) _, pow_two_pow_half (c ^ 2 / b) _, pow_two_pow_half (b ^ 2 / a) _],
{
refine congr_fun (congr_arg pow _) _,
field_simp [ne_of_gt hb₃, ne_of_gt hc₃, pow_succ' c 2, ne_of_gt h₀.2.2, mul_div_cancel_left],
ring_nf,
},
{
refine congr_fun (congr_arg pow _) _,
field_simp [ne_of_gt ha₃, ne_of_gt hb₃, pow_succ' b 2, ne_of_gt h₀.2.1, mul_div_cancel_left],
ring_nf,
},
{
refine congr_fun (congr_arg pow _) _,
field_simp [ne_of_gt hc₃, ne_of_gt hb₃, pow_succ' a 2, ne_of_gt h₀.1, mul_div_cancel_left],
ring_nf,
},
exact div_pos (pow_pos h₀.2.1 2) h₀.1,
exact div_pos (pow_pos h₀.2.2 2) h₀.2.1,
exact div_pos (pow_pos h₀.1 2) h₀.2.2,
},
ring,
end


The line of field_simp [ne_of_gt hb₃, ne_of_gt hc₃, pow_succ' c 2, ne_of_gt h₀.2.2, mul_div_cancel_left], helps me out to convert an equality of b ^ 3 * a / c ^ 3 * (a ^ 3 * c / b ^ 3) = (a ^ 2 / c) ^ 2 to b ^ 3 * a * (a ^ 3 * c) * c ^ 2 = (a ^ 2) ^ 2 * (c ^ 2 * c * b ^ 3). Not sure if this you're referring to?

#### Huỳnh Trần Khanh (Jun 10 2021 at 12:23):

Just wondering: what's with the absurdly long theorem name? Mathlib theorem names tend to encode the formal statement of the theorem and I understand that you want to follow that convention, however I think this is very extreme.

#### Huỳnh Trần Khanh (Jun 10 2021 at 12:24):

As a side note, I tend to call everything a lemma because I'm not a mathematician, LOL. Only mathematicians can prove theorems. I'm just a mere programmer knowing absolutely nothing about proper mathematics.

#### Huỳnh Trần Khanh (Jun 10 2021 at 12:25):

Even though I know how to prove this inequality :clown:

#### Kevin Buzzard (Jun 10 2021 at 12:25):

you won't like Lean 4 then :-)

#### Kunhao Zheng (Jun 10 2021 at 12:33):

Huỳnh Trần Khanh said:

Just wondering: what's with the absurdly long theorem name? Mathlib theorem names tend to encode the formal statement of the theorem and I understand that you want to follow that convention, however I think this is very extreme.

Somehow that's a naming convention we adapt from the metamath system to keep it aligned with statements written in that system (https://github.com/openai/miniF2F), I admit it's a bit tedious and longer but you could know what it tells us by reading the name. I once wanted to come up with another naming convention but I fell back into it:( so if you have any suggestions I will be very happy!

#### Johan Commelin (Jun 10 2021 at 12:39):

@Kunhao Zheng The mathlib name would probably be sq_div_add_sq_div_add_sq_div_le

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:22):

@Kunhao Zheng When you have a goal that can be closed simply by substituting variables, try cc. The cc (congruence closure) tactic is specifically designed for this.

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:23):

import data.real.basic

lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d := by cc


#### Huỳnh Trần Khanh (Jun 10 2021 at 13:25):

The congruence closure tactic is based on the union-find data structure, which is very popular in competitive programming. You are from China, right? I know Chinese people are competitive programming gods!

#### Kunhao Zheng (Jun 10 2021 at 16:17):

Huỳnh Trần Khanh said:

The congruence closure tactic is based on the union-find data structure, which is very popular in competitive programming. You are from China, right? I know Chinese people are competitive programming gods!

Thank you for the hint! You're right. Though I have a CS background but I'm not so good at the competition :grinning_face_with_smiling_eyes:

Last updated: Dec 20 2023 at 11:08 UTC