mongePointVSubFaceCentroidWeightsWithCircumcenter

English

The Monge point of an (n+2)-simplex equals the affine combination of its pointsWithCircumcenter with weights mongePointWeightsWithCircumcenter n.

Русский

MongePoint (n+2)-многоугольника равен аффинной комбинации точекWithCircumcenter со весами mongePointWeightsWithCircumcenter n.

LaTeX

$$$$ s.mongePoint = (univ : Finset (PointsWithCircumcenterIndex (n + 2))).affineCombination \mathbb{R} \bigl(s.pointsWithCircumcenter\bigr) (mongePointWeightsWithCircumcenter n). $$$$

Lean4

/-- The weights for the Monge point of an (n+2)-simplex, minus the
centroid of an n-dimensional face, in terms of
`pointsWithCircumcenter`.  This definition is only valid when `i₁ ≠ i₂`. -/
def mongePointVSubFaceCentroidWeightsWithCircumcenter {n : ℕ} (i₁ i₂ : Fin (n + 3)) :
    PointsWithCircumcenterIndex (n + 2) → ℝ
  | pointIndex i => if i = i₁ ∨ i = i₂ then ((n + 1 : ℕ) : ℝ)⁻¹ else 0
  | circumcenterIndex => -2 / ((n + 1 : ℕ) : ℝ)

Похожие утверждения