norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul

English

If x ≠ 0 and r ≠ 0, then ⟪x, r·x⟫ℝ / (∥x∥ ∥r·x∥) = 1, i.e. the normalized inner product is maximally aligned.

Русский

Если x ≠ 0 и r ≠ 0, то ⟪x, r·x⟫ℝ / (∥x∥ ∥r·x∥) = 1.

LaTeX

$$$\frac{\langle x, r\cdot x\rangle}{\|x\| \|r\cdot x\|} = 1$ при $x \neq 0$ и $r \neq 0$$$

Lean4

/-- The inner product of a nonzero vector with a nonzero multiple of
itself, divided by the product of their norms, has absolute value
1. -/
theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) :
    ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1 := by
  have hx' : ‖x‖ ≠ 0 := by simp [hx]
  have hr' : ‖r‖ ≠ 0 := by simp [hr]
  rw [inner_smul_right, norm_mul, ← inner_self_re_eq_norm, inner_self_eq_norm_mul_norm, norm_smul]
  rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm, mul_div_cancel_right₀ _ hr',
    div_self hx']

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