how to prove this in a simple and clear way?

Stream: new members

[Zihao Zhang]

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt

section

-- 定义等式左边部分，依赖于 a, b, c
noncomputable def lhs (a b c : ℝ) : ℝ :=
  √ (((a ^ 3) ^ (2 / 3) + (b ^ 3) ^ (2 / 3) + (c ^ 3) ^ (2 / 3)) ^ 3 /
      ((b + 3 * a) ^ 2 + (c + 3 * b) ^ 2 + (a + 3 * c) ^ 2)) +
  5 * a ^ 3 / (a + 3 * c) +
  5 * b ^ 3 / (b + 3 * a) +
  5 * c ^ 3 / (c + 3 * b)

-- 标记为 noncomputable，因为 sqrt 函数涉及实数计算
noncomputable def rhs (a b c : ℝ) : ℝ :=
  √ (a ^ 2 + b ^ 2 + c ^ 2) /
  √ (10 * a ^ 2 + 10 * b ^ 2 + 10 * c ^ 2 + 6 * a * b + 6 * a * c + 6 * b * c) *
  (a ^ (1 + 1) + c ^ (1 + 1) + b ^ (1 + 1)) +
  (5 * a ^ 3 / (a + 3 * c) +
  5 * b ^ 3 / (3 * a + b) +
  5 * c ^ 3 / (3 * b + c))

-- 证明等式 lhs a b c = rhs a b c
example complex_eq (a b c : ℝ) : lhs a b c = rhs a b c :=by
  rw [lhs,rhs]


end

[Kevin Buzzard]

Is this definitely true?

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt

section

-- 定义等式左边部分，依赖于 a, b, c
noncomputable def lhs (a b c : ℝ) : ℝ :=
  √ (((a ^ 3) ^ (2 / 3) + (b ^ 3) ^ (2 / 3) + (c ^ 3) ^ (2 / 3)) ^ 3 /
      ((b + 3 * a) ^ 2 + (c + 3 * b) ^ 2 + (a + 3 * c) ^ 2)) +
  5 * a ^ 3 / (a + 3 * c) +
  5 * b ^ 3 / (b + 3 * a) +
  5 * c ^ 3 / (c + 3 * b)

-- 标记为 noncomputable，因为 sqrt 函数涉及实数计算
noncomputable def rhs (a b c : ℝ) : ℝ :=
  √ (a ^ 2 + b ^ 2 + c ^ 2) /
  √ (10 * a ^ 2 + 10 * b ^ 2 + 10 * c ^ 2 + 6 * a * b + 6 * a * c + 6 * b * c) *
  (a ^ (1 + 1) + c ^ (1 + 1) + b ^ (1 + 1)) +
  (5 * a ^ 3 / (a + 3 * c) +
  5 * b ^ 3 / (3 * a + b) +
  5 * c ^ 3 / (3 * b + c))

-- 证明等式 lhs a b c = rhs a b c
example (a b c : ℝ) : lhs a b c = rhs a b c := by
  rw [lhs,rhs]
  rw [add_comm b, add_comm c]
  repeat rw [← add_assoc]
  congr 3
  field_simp
  ring_nf
  repeat rw [← add_mul]
  rw [add_mul]
  nth_rw 11 [mul_comm]
  rw [← mul_assoc]
  congr 1
  -- goal now looks false
  sorry

[Edward van de Meent]

presumably, the 2/3 in the exponents should be cast to Real first...

[Kevin Buzzard]

You're right but this might not be enough: if $a^3<0$ then is it true that $(a^3)^{(2/3)}=a^2$ if the 2/3 is a real?

If we had a type for rational numbers with odd denominator, then one could raise a real number to such a power and get a good answer for negative numbers. But there's no sensible answer to (-1)^{1/2} and hence one can't expect (-1)^r to make sense if r is a term of a type which has got a 1/2 in.

[Edward van de Meent]

indeed, Real.rpow_mul requires a nonneg parameter...

[Zihao Zhang]

Kevin Buzzard said:

Is this definitely true?

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt

section

-- 定义等式左边部分，依赖于 a, b, c
noncomputable def lhs (a b c : ℝ) : ℝ :=
  √ (((a ^ 3) ^ (2 / 3) + (b ^ 3) ^ (2 / 3) + (c ^ 3) ^ (2 / 3)) ^ 3 /
      ((b + 3 * a) ^ 2 + (c + 3 * b) ^ 2 + (a + 3 * c) ^ 2)) +
  5 * a ^ 3 / (a + 3 * c) +
  5 * b ^ 3 / (b + 3 * a) +
  5 * c ^ 3 / (c + 3 * b)

-- 标记为 noncomputable，因为 sqrt 函数涉及实数计算
noncomputable def rhs (a b c : ℝ) : ℝ :=
  √ (a ^ 2 + b ^ 2 + c ^ 2) /
  √ (10 * a ^ 2 + 10 * b ^ 2 + 10 * c ^ 2 + 6 * a * b + 6 * a * c + 6 * b * c) *
  (a ^ (1 + 1) + c ^ (1 + 1) + b ^ (1 + 1)) +
  (5 * a ^ 3 / (a + 3 * c) +
  5 * b ^ 3 / (3 * a + b) +
  5 * c ^ 3 / (3 * b + c))

-- 证明等式 lhs a b c = rhs a b c
example (a b c : ℝ) : lhs a b c = rhs a b c := by
  rw [lhs,rhs]
  rw [add_comm b, add_comm c]
  repeat rw [← add_assoc]
  congr 3
  field_simp
  ring_nf
  repeat rw [← add_mul]
  rw [add_mul]
  nth_rw 11 [mul_comm]
  rw [← mul_assoc]
  congr 1
  -- goal now looks false
  sorry

I think the ring_nf leads to the wrong goal，the goal before and after it is not equivalent，for example,the √27 is strange enough.

[Kevin Buzzard]

I think that actually the questioner asked the wrong question :-) The goals are equivalent, it's just that the actual maths question has not been correctly translated into lean. As has been already noted, all those 2/3's are 0.

[Zihao Zhang]

@Kevin Buzzard
I changed the version,is it provale now?

import Mathlib

open Real

local macro_rules | `($x / $y)  => `(HDiv.hDiv ($x : ℝ) ($y : ℝ))

theorem test {a b c : ℝ} (anonneg:a≥0)(bnonneg:b≥0)(cnonneg:c≥0): sqrt (((a ^ 3) ^ (2 / 3) + (b ^ 3) ^ (2 / 3) + (c ^ 3) ^ (2 / 3)) ^ 3 / ((b + 3 * a) ^ 2 + (c + 3 * b) ^ 2 + (a + 3 * c) ^ 2)) + 5 * a ^ 3 / (a + 3 * c) + 5 * b ^ 3 / (b + 3 * a) + 5 * c ^ 3 / (c + 3 * b) = sqrt (a ^ 2 + b ^ 2 + c ^ 2) / sqrt (10 * a ^ 2 + 10 * b ^ 2 + 10 * c ^ 2 + 6 * a * b + 6 * a * c + 6 * b * c) * (a ^ (1 + 1) + c ^ (1 + 1) + b ^ (1 + 1)) + (5 * a ^ 3 / (a + 3 * c) + 5 * b ^ 3 / (3 * a + b) + 5 * c ^ 3 / (3 * b + c)) := by

[cairunze cairunze]

image.png
i'm not sure i convert your formula correctly, if available, maybe you can verify this using, say Mathematica/Maple/Matlab etc first?