English
The Monge point is orthogonal to the difference of two non-equal vertices when you subtract the centroid from the Monge point with respect to the corresponding face.
Русский
MongePoint ⟂ разности двух вершин по отношению к центроиду монге по соответствующей грани.
LaTeX
$$$$ \langle M - G_{face}, P_i - P_j \rangle = 0 $$$$
Lean4
/-- The Monge point of an (n+2)-simplex, minus the centroid of an
n-dimensional face, is orthogonal to the difference of the two
vertices not in that face. -/
theorem inner_mongePoint_vsub_face_centroid_vsub {n : ℕ} (s : Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)} :
⟪s.mongePoint -ᵥ ({ i₁, i₂ }ᶜ : Finset (Fin (n + 3))).centroid ℝ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0 :=
by
by_cases h : i₁ = i₂
· simp [h]
simp_rw [mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter s h,
point_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub]
have hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0 := by simp
rw [inner_weightedVSub _ (sum_mongePointVSubFaceCentroidWeightsWithCircumcenter h) _ hs, sum_pointsWithCircumcenter,
pointsWithCircumcenter_eq_circumcenter]
simp only [mongePointVSubFaceCentroidWeightsWithCircumcenter, pointsWithCircumcenter_point]
let fs : Finset (Fin (n + 3)) := { i₁, i₂ }
have hfs : ∀ i : Fin (n + 3), i ∉ fs → i ≠ i₁ ∧ i ≠ i₂ :=
by
intro i hi
constructor <;> · intro hj; simp [fs, ← hj] at hi
rw [← sum_subset fs.subset_univ _]
· simp_rw [sum_pointsWithCircumcenter, pointsWithCircumcenter_eq_circumcenter, pointsWithCircumcenter_point,
Pi.sub_apply, pointWeightsWithCircumcenter]
rw [← sum_subset fs.subset_univ _]
· simp_rw [fs, sum_insert (notMem_singleton.2 h), sum_singleton]
repeat rw [← sum_subset fs.subset_univ _]
· simp_rw [fs, sum_insert (notMem_singleton.2 h), sum_singleton]
simp [h, Ne.symm h, dist_comm (s.points i₁)]
all_goals intro i _ hi; simp [hfs i hi]
· intro i _ hi
simp [hfs i hi]
· intro i _ hi
simp [hfs i hi]
