English
For any i, j, the inner product between the altitude foot vectors exceeds the negated product of their heights: -(height_i height_j) < ⟪p_i−foot_i, p_j−foot_j⟫.
Русский
Для любых i, j скалярное произведение между векторами p_i−foot_i и p_j−foot_j больше чем −(height_i height_j).
LaTeX
$$$-(s.\\text{height}(i) \\cdot s.\\text{height}(j)) < ⟪s.\\text{points}(i)-ᵥ s.\\text{altitudeFoot}(i),\, s.\\text{points}(j)-ᵥ s.\\text{altitudeFoot}(j)⟫$$$
Lean4
/-- The inner product of two altitudes has value strictly greater than the negated product of
their lengths.
-/
theorem neg_mul_lt_inner_vsub_altitudeFoot (i j : Fin (n + 1)) :
-(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ :=
by
obtain rfl | hij := eq_or_ne i j
· rw [real_inner_self_eq_norm_sq]
refine lt_of_lt_of_le (b := 0) ?_ ?_
· rw [neg_lt_zero]
positivity
· positivity
rw [neg_lt]
refine lt_of_abs_lt ?_
rw [abs_neg]
exact abs_inner_vsub_altitudeFoot_lt_mul s hij
