English
For distinct indices i ≠ j, the absolute value of the inner product between the edge i−j and the altitude foot vectors is strictly less than the product of the heights: |⟪p_i−foot_i, p_j−foot_j⟫| < height_i height_j.
Русский
Для различных i ≠ j модуль скалярного произведения между векторами p_i−foot_i и p_j−foot_j строго меньше произведения высот: |⟪p_i−foot_i, p_j−foot_j⟫| < height_i height_j.
LaTeX
$$|\\langle s.\\text{points}(i)-s.\\text{altitudeFoot}(i), s.\\text{points}(j)-s.\\text{altitudeFoot}(j) \\rangle| < s.\\text{height}(i) \\cdot s.\\text{height}(j)$$
Lean4
/-- The inner product of two distinct altitudes has absolute value strictly less than the product of
their lengths.
Equivalently, neither vector is a multiple of the other; the angle between them is not 0 or π. -/
theorem abs_inner_vsub_altitudeFoot_lt_mul {i j : Fin (n + 1)} (hij : i ≠ j) :
|⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j :=
by
apply lt_of_le_of_ne
· convert abs_real_inner_le_norm _ _ using 1
simp only [dist_eq_norm_vsub, height]
· simp_rw [height, dist_eq_norm_vsub]
rw [← Real.norm_eq_abs, ne_eq, norm_inner_eq_norm_iff (by simp) (by simp)]
rintro ⟨r, hr, h⟩
suffices s.points j -ᵥ s.altitudeFoot j = 0 by simp at this
rw [← Submodule.mem_bot ℝ, ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
refine ⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩
· refine SetLike.le_def.1 (affineSpan_mono _ ?_) (Subtype.property _)
simp
· rw [SetLike.mem_coe]
have hk : ∃ k, k ≠ i ∧ k ≠ j :=
Fin.exists_ne_and_ne_of_two_lt i j (by linarith only [Nat.AtLeastTwo.one_lt (n := n)])
have hs :
vectorSpan ℝ (Set.range s.points) =
vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points) :=
by
rcases hk with ⟨k, hki, hkj⟩
have hki' : s.points k ∈ Set.range (s.faceOpposite i).points :=
by
rw [range_faceOpposite_points]
exact Set.mem_image_of_mem _ hki
have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points :=
by
rw [range_faceOpposite_points]
exact Set.mem_image_of_mem _ hkj
have hs : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points :=
by
simp only [range_faceOpposite_points, ← Set.image_union]
simp_rw [← Set.image_univ, ← Set.compl_inter]
rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
simpa using hij.symm
convert AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'
rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]
refine ⟨?_, ?_⟩
· rw [h, ← direction_affineSpan]
exact Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
· rw [← direction_affineSpan]
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
