English
In any quadrilateral A,B,C,D in a metric space, the product of diagonals AC and BD is at most the sum of products AB·CD and BC·AD. Equality holds for cyclic convex quadrilaterals.
Русский
В любой невыпуклой четырехугольник ABCD в метрическом пространстве произведение диагоналей AC и BD не превосходит суммы произведений сторон AB·CD и BC·AD. Равенство достигается для выпуклого цыклического четырехугольника.
LaTeX
$$$d(A,C)\cdot d(B,D) \le d(A,B)\cdot d(C,D) + d(B,C)\cdot d(A,D)$$$
Lean4
/-- **Ptolemy's inequality**: in a quadrangle `ABCD`, `|AC| * |BD| ≤ |AB| * |CD| + |BC| * |AD|`. If
`ABCD` is a convex cyclic polygon, then this inequality becomes an equality, see
`EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical`. -/
theorem mul_dist_le_mul_dist_add_mul_dist (a b c d : P) :
dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d := by
-- If one of the points `b`, `c`, `d` is equal to `a`, then the inequality is trivial.
rcases eq_or_ne b a with (rfl | hb)
· rw [dist_self, zero_mul, zero_add]
rcases eq_or_ne c a with (rfl | hc)
· rw [dist_self, zero_mul]
positivity
rcases eq_or_ne d a with (rfl | hd)
·
rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
/- Otherwise, we apply the triangle inequality to `EuclideanGeometry.inversion a 1 b`,
`EuclideanGeometry.inversion a 1 c`, and `EuclideanGeometry.inversion a 1 d`. -/
have H := dist_triangle (inversion a 1 b) (inversion a 1 c) (inversion a 1 d)
rw [dist_inversion_inversion hb hd, dist_inversion_inversion hb hc, dist_inversion_inversion hc hd, one_pow] at H
rw [← dist_pos] at hb hc hd
rw [← div_le_div_iff_of_pos_right (mul_pos hb (mul_pos hc hd))]
convert H using 1 <;> simp [field, dist_comm a]; ring
