English
Let x,y ≠ 0. Then ⟪x,y⟫ = ∥x∥ ∥y∥ if and only if y = r x for some r ≠ 0 in the scalar field, i.e. x and y are positively collinear.
Русский
Пусть x,y ≠ 0. Тогда ⟪x,y⟫ = ∥x∥ ∥y∥ тогда и только тогда, когда ∃r ≠ 0: y = r x, т.е. x и y положительно коллинеарны.
LaTeX
$$$⟨x,y⟩ = ∥x∥ ∥y∥ \quad\Longleftrightarrow\quad ∃ r\neq 0:\ y = r x$$
Lean4
/-- Formula for the distance between the images of two nonzero points under an inversion with center
zero. See also `EuclideanGeometry.dist_inversion_inversion` for inversions around a general
point. -/
theorem dist_div_norm_sq_smul {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) (R : ℝ) :
dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y :=
calc
dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = √(‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2) := by
rw [dist_eq_norm, sqrt_sq (norm_nonneg _)]
_ = √((R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2) :=
(congr_arg (√·) <|
by
simp [field, sq, norm_sub_mul_self_real, norm_smul, real_inner_smul_left, inner_smul_right,
Real.norm_of_nonneg (mul_self_nonneg _), -mul_eq_mul_left_iff]
ring)
_ = R ^ 2 / (‖x‖ * ‖y‖) * dist x y := by rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm] <;> positivity
