Jensen_square_div_3vars

[GanjinZero]

theorem Jensen_square_div_3vars (u v w : ℝ) (hu : u > 0) (hv : v > 0) (hw : w > 0) : (1 / u ^ 2 + 1 / v ^ 2 + 1 / w ^ 2) / 3 ≤ 9 / (u + v + w) ^ 2 := by
  sorry

This theorem with u=1, v=1, w=2 is wrong.

[RexWzh]

I just noticed that about half of the proofs (73/130) use the SorryAx axiom, with four of them specifically using Jensen_square_div_3vars.

Here is an example (P2 in INT_MO.lean), which uses other sorry theorem like Titu_variant1_right_4vars:

theorem Titu_variant1_right_4vars (u1 u2 u3 u4 v1 v2 v3 v4 k l left : ℝ)
  (hv1 : v1 > 0) (hv2 : v2 > 0) (hv3 : v3 > 0) (hv4 : v4 > 0) (hk : k > 0)
  (h : left ≤ k * ((u1 + u2 + u3 + u4) ^ 2 / (u1 * v1 + u2 * v2 + u3 * v3 + u4 * v4)) + l) :
  left ≤ k * (u1 / v1 + u2 / v2 + u3 / v3 + u4 / v4) + l := by
    suffices (u1 + u2 + u3 + u4) ^ 2 / (u1 * v1 + u2 * v2 + u3 * v3 + u4 * v4)
      ≤ (u1 / v1 + u2 / v2 + u3 / v3 + u4 / v4) by nlinarith
    sorry

The high proportion of sorry usages (56%) could reduce the reliability of these proofs. It might be worth prioritizing the completion of these proofs in upcoming updates.

[Lizn-zn]

Thank you for reporting this issue! We’ve now corrected the error in Jensen_square_div_3vars and updated the involved proofs.

We’d also like to extend our thanks to RexWzh (@RexWzh) for the valuable suggestion — we will fill SorryAx axioms in future updates.