English
For a simplex s and weights w with sum 1, the signedInfDist equals the weighted norm of the displacement of the barycenter vertex against the opposite face projection.
Русский
Для простейшего s и весов w сумму которых равна 1, s.signedInfDist на аффинной комбинации равна взвешенной норме вектора смещения вершины к проекции противоположной грани.
LaTeX
$$$s.signedInfDist i (\text{affineCombination}(s.points, w)) = w_i \cdot \| (s.points i) -\! (s.faceOpposite i).orthogonalProjectionSpan (s.points i) \|$$$
Lean4
theorem signedInfDist_affineCombination {w : Fin (n + 1) → ℝ} (h : ∑ i, w i = 1) :
s.signedInfDist i (Finset.univ.affineCombination ℝ s.points w) =
w i * ‖s.points i -ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖ :=
by
rw [← ContinuousAffineMap.coe_toAffineMap, Finset.map_affineCombination _ _ _ h,
Finset.univ.affineCombination_apply_eq_lineMap_sum w ((s.signedInfDist i).toAffineMap ∘ s.points) 0
‖s.points i -ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖ { i } h]
· simp [AffineMap.lineMap_apply]
· simp [signedInfDist_apply_self]
· simp only [Finset.mem_sdiff, Finset.mem_univ, Finset.mem_singleton, true_and, Function.comp_apply]
intro j hj
exact s.signedInfDist_apply_of_ne hj
