eq_of_norm_le_re_inner_eq_norm_sq

English

If ||x|| ≤ ||y|| and Re⟪x,y⟫ = ||y||^2, then x = y.

Русский

Если ∥x∥ ≤ ∥y∥ и Re⟪x,y⟫ = ∥y∥^2, то x = y.

LaTeX

$$$\|x\| \leq \|y\| \quad\land\quad \operatorname{Re}\langle x,y\rangle = \|y\|^2 \Rightarrow x = y$$$

Lean4

/-- The sphere of radius `r = ‖y‖` is tangent to the plane `⟪x, y⟫ = ‖y‖ ^ 2` at `x = y`. -/
theorem eq_of_norm_le_re_inner_eq_norm_sq {x y : E} (hle : ‖x‖ ≤ ‖y‖) (h : re ⟪x, y⟫ = ‖y‖ ^ 2) : x = y :=
  by
  suffices H : re ⟪x - y, x - y⟫ ≤ 0 by rwa [re_inner_self_nonpos, sub_eq_zero] at H
  have H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 := by gcongr
  have H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2 := by rwa [← inner_conj_symm, conj_re]
  simpa [inner_sub_left, inner_sub_right, ← norm_sq_eq_re_inner, h, H₂] using H₁

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