English
The transitive composition of two equivalences equals the direct equivalence corresponding to the composition of index bijections.
Русский
Транзитивное сочетание двух эквивалентностей эквивалентно прямой эквивелентности, соответствующей составу биекций индексов.
LaTeX
$$$(hv \\equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e\\.trans e')$$$
Lean4
/-- Bessel's inequality for finite sums. -/
theorem sum_inner_products_le {s : Finset ι} (hv : Orthonormal 𝕜 v) : ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2 :=
by
have h₂ : (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) = (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫ : 𝕜) := by
classical exact hv.inner_left_right_finset
have h₃ : ∀ z : 𝕜, re (z * conj z) = ‖z‖ ^ 2 := by
intro z
simp only [mul_conj]
norm_cast
suffices hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
by
rw [← sub_nonneg, ← hbf]
simp only [norm_nonneg, pow_nonneg]
rw [@norm_sub_sq 𝕜, sub_add]
simp only [@InnerProductSpace.norm_sq_eq_re_inner 𝕜 E, inner_sum, sum_inner]
simp only [inner_smul_right, two_mul, inner_smul_left, inner_conj_symm, ← mul_assoc, h₂, add_sub_cancel_right,
sub_right_inj]
simp only [map_sum, ← inner_conj_symm x, ← h₃]
