norm_sub_eq_abs_sub_norm_iff_angle_eq_zero

English

If angle x y = 0, then ‖x − y‖ = |‖x‖ − ‖y‖|.

Русский

Если угол x y равен 0, то ‖x − y‖ = |‖x‖ − ‖y‖|.

LaTeX

$$angle x y = 0 → ‖x - y‖ = |‖x‖ - ‖y‖|$$

Lean4

/-- The norm of the difference of two non-zero vectors equals the absolute value
of the difference of their norms if and only the angle between the two vectors is 0. -/
theorem norm_sub_eq_abs_sub_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ‖x - y‖ = |‖x‖ - ‖y‖| ↔ angle x y = 0 :=
  by
  refine ⟨fun h => ?_, norm_sub_eq_abs_sub_norm_of_angle_eq_zero⟩
  rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]
  have h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2 := by
    rw [h]
    exact sq_abs (‖x‖ - ‖y‖)
  rw [norm_sub_pow_two_real] at h1
  calc
    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
    _ = ‖x‖ * ‖y‖ := by ring

Похожие утверждения