English
If a point p1 lies on a sphere s and a point p2 is no farther from the center than the radius, then the inner product ⟪p1−p2, p1−center⟫ is nonnegative.
Русский
Если точка p1 лежит на сфере s, а точка p2 не дальше радиуса от центра, то внутрискорость ⟪p1−p2, p1−центр⟫ неотрицательна.
LaTeX
$$$p_1\in s\text{ and } dist(p_2, center) \le s.radius \Rightarrow 0 \le \langle p_1-p_2, p_1-center\rangle$$$
Lean4
/-- Given a point on a sphere and a point not outside it, the inner product between the
difference of those points and the radius vector is positive unless the points are equal. -/
theorem inner_pos_or_eq_of_dist_le_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
(hp₂ : dist p₂ s.center ≤ s.radius) : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂ :=
by
by_cases h : p₁ = p₂; · exact Or.inr h
refine Or.inl ?_
rw [mem_sphere] at hp₁
rw [← vsub_sub_vsub_cancel_right p₁ p₂ s.center, inner_sub_left, real_inner_self_eq_norm_mul_norm, sub_pos]
refine lt_of_le_of_ne ((real_inner_le_norm _ _).trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))) ?_
· rwa [← dist_eq_norm_vsub, ← dist_eq_norm_vsub, hp₁]
· rcases hp₂.lt_or_eq with (hp₂' | hp₂')
· refine ((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right ?_ ?_)).ne
· rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
· rw [norm_pos_iff, vsub_ne_zero]
rintro rfl
rw [← hp₁] at hp₂'
refine (dist_nonneg.not_gt : ¬dist p₂ s.center < 0) ?_
simpa using hp₂'
· rw [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
nth_rw 1 [← hp₂']
rw [Ne, inner_eq_norm_mul_iff_real, hp₂', ← sub_eq_zero, ← smul_sub, vsub_sub_vsub_cancel_right, ← Ne,
smul_ne_zero_iff, vsub_ne_zero, and_iff_left (Ne.symm h), norm_ne_zero_iff, vsub_ne_zero]
rintro rfl
refine h (Eq.symm ?_)
simpa using hp₂'
