real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul

English

If x ≠ 0 and 0 < r, then ⟪x, r·x⟫ℝ / (∥x∥ ∥r·x∥) = 1.

Русский

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

LaTeX

$$$\frac{\langle x, r\cdot x\rangle_{\mathbb{R}}}{\|x\| \|r\cdot x\|} = 1\quad \text{ при } x\neq 0,\; r>0$$$

Lean4

/-- The inner product of a nonzero vector with a positive multiple of
itself, divided by the product of their norms, has value 1. -/
theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {x : F} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) :
    ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1 :=
  by
  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|, mul_assoc,
    abs_of_nonneg hr.le, div_self]
  exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

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