English
For any l ∈ ι →₀ 𝕜, the inner product with a basis vector picks out the corresponding coefficient: ⟪v_i, linearCombination v l⟫ = l_i.
Русский
Для любого l ∈ ι →₀ 𝕜 скалярное произведение с вектором v_i выбирает соответствующий коэффициент: ⟪v_i, linearCombination v l⟫ = l_i.
LaTeX
$$$\text{Let } l \in ι \to 𝕜.\; \langle v_i, \operatorname{linearCombination} 𝕜 v l \rangle = l_i$$$
Lean4
/-- `if ... then ... else` characterization of an indexed set of vectors being orthonormal. (Inner
product equals Kronecker delta.) -/
theorem orthonormal_iff_ite [DecidableEq ι] {v : ι → E} :
Orthonormal 𝕜 v ↔ ∀ i j, ⟪v i, v j⟫ = if i = j then (1 : 𝕜) else (0 : 𝕜) :=
by
constructor
· intro hv i j
split_ifs with h
· simp [h, inner_self_eq_norm_sq_to_K, hv.norm_eq_one]
· exact hv.inner_eq_zero h
· intro h
constructor
· intro i
have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by simp [@norm_sq_eq_re_inner 𝕜, h i i]
have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _
have h₂ : (0 : ℝ) ≤ 1 := zero_le_one
rwa [sq_eq_sq₀ h₁ h₂] at h'
· intro i j hij
simpa [hij] using h i j
