English
The sum over all vertices of the inverse height squared, scaled by the vector difference to the altitude foot, vanishes.
Русский
Сумма по вершинам: h_i^{-2}(p_i - altitudeFoot_i) равна нулю.
LaTeX
$$$\displaystyle \sum_i (h_i)^{-2} \cdot (p_i - v_i) = 0$$$
Lean4
theorem sum_inv_height_sq_smul_vsub_eq_zero : ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) = 0 :=
by
suffices ∀ i, i ≠ 0 → ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
by
rw [← Submodule.mem_bot ℝ, ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
refine
⟨Submodule.sum_smul_mem _ _ fun i hi ↦
vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan (mem_affineSpan _ (Set.mem_range_self _))
(altitudeFoot_mem_affineSpan _ _),
?_⟩
rw [vectorSpan_range_eq_span_range_vsub_right_ne _ _ 0, Submodule.span_range_eq_iSup, ← Submodule.iInf_orthogonal,
Submodule.coe_iInf, Set.mem_iInter]
intro i
rcases i with ⟨i, hi⟩
simpa only [SetLike.mem_coe, Submodule.mem_orthogonal_singleton_iff_inner_right, inner_sum] using this i hi
intro i hi
rw [← Finset.add_sum_erase _ _ (Finset.mem_univ 0), ←
Finset.add_sum_erase _ _ (Finset.mem_erase.2 ⟨hi, Finset.mem_univ _⟩), ← add_assoc]
convert add_zero _
· convert Finset.sum_const_zero with j hj
rw [real_inner_smul_right]
convert mul_zero _
rw [← Submodule.mem_orthogonal_singleton_iff_inner_right]
refine SetLike.le_def.1 (Submodule.orthogonal_le ?_) (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
rw [Submodule.span_singleton_le_iff_mem, direction_affineSpan]
simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj
refine vsub_mem_vectorSpan _ ?_ ?_ <;> simp only [range_faceOpposite_points, Set.mem_image]
· exact ⟨i, hj.1.symm, rfl⟩
· exact ⟨0, hj.2.symm, rfl⟩
· rw [inner_smul_right, inner_smul_right, inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi, ← neg_vsub_eq_vsub_rev,
inner_neg_left, inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi.symm, mul_neg, inv_pow]
simp [height]
