English
If i1 ≠ i2, the sum over i of reflectionCircumcenterWeightsWithCircumcenter i1 i2 i equals 1.
Русский
Если i1 ≠ i2, то сумма reflectionCircumcenterWeightsWithCircumcenter i1 i2 i по i равна 1.
LaTeX
$$$\sum_i reflectionCircumcenterWeightsWithCircumcenter i1 i2 i = 1\quad(i_1\neq i_2)$$$
Lean4
/-- The reflection of the circumcenter of a simplex in an edge, in
terms of `pointsWithCircumcenter`. -/
theorem reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P n)
{i₁ i₂ : Fin (n + 1)} (h : i₁ ≠ i₂) :
reflection (affineSpan ℝ (s.points '' { i₁, i₂ })) s.circumcenter =
(univ : Finset (PointsWithCircumcenterIndex n)).affineCombination ℝ s.pointsWithCircumcenter
(reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) :=
by
have hc : #{ i₁, i₂ } = 2 := by
simp [h]
-- Making the next line a separate definition helps the elaborator:
set W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' { i₁, i₂ })
have h_faces : (orthogonalProjection W s.circumcenter : P) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter) :=
by
apply eq_orthogonalProjection_of_eq_subspace
simp [W]
rw [EuclideanGeometry.reflection_apply, h_faces, s.orthogonalProjection_circumcenter hc, circumcenter_eq_centroid,
s.face_centroid_eq_centroid hc, centroid_eq_affineCombination_of_pointsWithCircumcenter,
circumcenter_eq_affineCombination_of_pointsWithCircumcenter, ← @vsub_eq_zero_iff_eq V, affineCombination_vsub,
weightedVSub_vadd_affineCombination, affineCombination_vsub, weightedVSub_apply, sum_pointsWithCircumcenter]
simp_rw [Pi.sub_apply, Pi.add_apply, Pi.sub_apply, sub_smul, add_smul, sub_smul, centroidWeightsWithCircumcenter,
circumcenterWeightsWithCircumcenter, reflectionCircumcenterWeightsWithCircumcenter, ite_smul, zero_smul, sub_zero,
apply_ite₂ (· + ·), add_zero, ← add_smul, hc, zero_sub, neg_smul, sub_self, add_zero]
convert sum_const_zero
norm_num
