English
For vectors x,y,z with x a scalar multiple of y and ⟪z−y,y⟫=0 and ⟪z,x⟫=0, one has ‖x−y‖‖x+y‖ = |‖z+y‖^2 − ‖z−x‖^2|.
Русский
Для векторов x,y,z, где x кратен y и ⟪z−y,y⟫=0, ⟪z,x⟫=0, имеет место ‖x−y‖‖x+y‖ = |‖z+y‖^2 − ‖z−x‖^2|.
LaTeX
$$$\exists k\in\mathbb{R},\ x=k\,y\quad\land\ ‖z-y‖=‖z+y‖\Rightarrow ‖x-y‖\,‖x+y‖=\big|‖z+y‖^2-‖z-x‖^2\big|$$$
Lean4
theorem mul_norm_eq_abs_sub_sq_norm {x y z : V} (h₁ : ∃ k : ℝ, x = k • y) (h₃ : ‖z - y‖ = ‖z + y‖) :
‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| :=
by
obtain ⟨r, hr⟩ := h₁
have hzy : ⟪z, y⟫ = 0 := by
rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two, eq_comm]
have hzx : ⟪z, x⟫ = 0 := by rw [hr, inner_smul_right, hzy, mul_zero]
calc
‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
_ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
_ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
_ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
_ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
_ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
_ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
