English
Let x,y ≠ 0. Then ||⟪x,y⟫|| = ||x|| ||y|| if and only if there exists a nonzero scalar r with y = r x.
Русский
Пусть x,y ≠ 0. Тогда ||⟪x,y⟫|| = ||x|| ||y|| тогда и только тогда, когда ∃ не нулевой скаляр r: y = r x.
LaTeX
$$$\|\langle x,y\rangle\| = \|x\| \|y\| \quad\Longleftrightarrow\quad \exists r \, (r \neq 0 \land y = r x)$$$
Lean4
theorem norm_inner_eq_norm_tfae (x y : E) :
List.TFAE
[‖⟪x, y⟫‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ r : 𝕜, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x] :=
by
tfae_have 1 → 2 := by
refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_
have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)
rw [← sq_eq_sq₀, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h <;> try positivity
simp only [@norm_sq_eq_re_inner 𝕜] at h
letI : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
erw [← InnerProductSpace.Core.cauchy_schwarz_aux (𝕜 := 𝕜) (F := E)] at h
rw [InnerProductSpace.Core.normSq_eq_zero, sub_eq_zero] at h
rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
rwa [inner_self_ne_zero]
tfae_have 2 → 3 := fun h => h.imp_right fun h' => ⟨_, h'⟩
tfae_have 3 → 1 := by
rintro (rfl | ⟨r, rfl⟩) <;> simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K, sq, mul_left_comm]
tfae_have 3 ↔ 4 := by simp only [Submodule.mem_span_singleton, eq_comm]
tfae_finish
