norm_add_eq_add_norm_iff_angle_eq_zero

English

For nonzero x,y, ‖x + y‖ = ‖x‖ + ‖y‖ if and only if angle x y = 0.

Русский

Для ненулевых x,y: ‖x + y‖ = ‖x‖ + ‖y‖ тогда и только тогда, когда угол x y = 0.

LaTeX

$$‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0 (для x ≠ 0, y ≠ 0)$$

Lean4

/-- The norm of the sum of two non-zero vectors equals the sum of their norms
if and only the angle between the two vectors is 0. -/
theorem norm_add_eq_add_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_add_eq_add_norm_of_angle_eq_zero⟩
  rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]
  obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x + y), add_nonneg (norm_nonneg x) (norm_nonneg y)
  rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_add_pow_two_real] at h
  calc
    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
    _ = ‖x‖ * ‖y‖ := by ring

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