English
For each vertex i, 1/h_i equals a sum over all j ≠ i of a scalar multiple involving inner products of vertex differences, scaled by h_i and h_j.
Русский
Для каждого i отношение 1/h_i равняется сумме по j ≠ i от коэффициента, зависящего от скалярного произведения разностей вершин, деленного на h_i h_j и умноженного на 1/h_j.
LaTeX
$$$ (h_i)^{-1} = \sum_{j \neq i} -\frac{\langle p_i - a_i, p_j - a_j \rangle}{h_i h_j} \cdot (h_j)^{-1} $$$
Lean4
/-- The inverse of the distance from one vertex to the opposite face, expressed as a sum of
multiples of that quantity for the other vertices. The multipliers, expressed here in terms of
inner products, are equal to the cosines of angles between faces (informally, the inverse
distances are proportional to the volumes of the faces and this is equivalent to expressing
the volume of a face as the sum of the signed volumes of projections of the other faces onto that
face). -/
theorem inv_height_eq_sum_mul_inv_dist (i : Fin (n + 1)) :
(s.height i)⁻¹ =
∑ j ∈ {k | k ≠ i},
-(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) *
(s.height j)⁻¹ :=
by
rw [← sub_eq_zero]
simp_rw [neg_mul]
rw [Finset.sum_neg_distrib, sub_neg_eq_add, Finset.filter_ne', Finset.sum_erase_eq_sub (Finset.mem_univ _),
real_inner_self_eq_norm_mul_norm, ← dist_eq_norm_vsub]
simp only [height, ne_eq, mul_eq_zero, dist_eq_zero, ne_altitudeFoot, or_self, not_false_eq_true, div_self, one_mul,
add_sub_cancel]
have h := s.sum_inv_height_sq_smul_vsub_eq_zero
apply_fun fun v ↦ (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, v⟫ at h
rw [inner_sum, Finset.mul_sum] at h
simp only [inner_zero_right, mul_zero, inner_smul_right, height] at h
convert h using 2 with j
ring
