English
The weight function mongePointVSubFaceCentroidWeightsWithCircumcenter assigns to each vertex 1/(n+1) and to the circumcenter -2/(n+1), while indexing by i₁ and i₂ marks the two distinguished vertices.
Русский
Функция весов mongePointVSubFaceCentroidWeightsWithCircumcenter присваивает каждому вершине 1/(n+1), а центроиду -2/(n+1); для двух помеченных вершин i₁,i₂ повторяется соответствующее правило.
LaTeX
$$$$ mongePointVSubFaceCentroidWeightsWithCircumcenter\ i_1\ i_2 = \{ i_1,i_2 \}^c \mapsto \dfrac{1}{n+1}, \text{circumcenter} \mapsto -\dfrac{2}{n+1}. $$$$
Lean4
/-- `mongePointVSubFaceCentroidWeightsWithCircumcenter` is the
result of subtracting `centroidWeightsWithCircumcenter` from
`mongePointWeightsWithCircumcenter`. -/
theorem mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub {n : ℕ} {i₁ i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) :
mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter { i₁, i₂ }ᶜ :=
by
ext i
obtain i | i := i
· rw [Pi.sub_apply, mongePointWeightsWithCircumcenter, centroidWeightsWithCircumcenter,
mongePointVSubFaceCentroidWeightsWithCircumcenter]
have hu : #{ i₁, i₂ }ᶜ = n + 1 := by simp [card_compl, Fintype.card_fin, h]
rw [hu]
by_cases hi : i = i₁ ∨ i = i₂ <;> simp [compl_eq_univ_sdiff, hi]
·
simp [mongePointWeightsWithCircumcenter, centroidWeightsWithCircumcenter,
mongePointVSubFaceCentroidWeightsWithCircumcenter]
