Match lhs and rhs of inequality

Stream: new members

[Kunhao Zheng]

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₅,
  have h₉ := add_le_add (add_le_add 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₃],
    refine congr (congr_arg has_add.add _) _,
    refine congr (congr_arg has_add.add _) _,
    {
      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]

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]

Do we have docs#has_le.le.trans_eq?

[Eric Wieser]

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

[Johan Commelin]

j.symm.le is j.ge

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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]

For increased opacity, this also works:

by convert h; exact eq.symm ‹_›

[Damiano Testa]

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]

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]

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]

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

[Kunhao Zheng]

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]

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

[Johan Commelin]

So the , is just \forall bla, blabla

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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₅,
  have h₉ := add_le_add (add_le_add 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 (congr_arg has_add.add _) _,
    refine congr (congr_arg has_add.add _) _,
    {
      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]

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]

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]

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

[Kevin Buzzard]

you won't like Lean 4 then :-)

[Kunhao Zheng]

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]

@Kunhao Zheng The mathlib name would probably be sq_div_add_sq_div_add_sq_div_le

[Huỳnh Trần Khanh]

@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]

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]

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]

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: