English
The inner product on the product is defined by the sum of inner products of coordinates: ⟪x, y⟫ = ∑_i ⟪x_i, y_i⟫_A.
Русский
Пусть скалярное произведение на произведении таково, что ⟪x, y⟫ = ∑_i ⟪x_i, y_i⟫_A.
LaTeX
$$$\\langle x, y \\rangle_A = \\sum_i \\langle x_i, y_i \\rangle_A$$$
Lean4
noncomputable instance : CStarModule A C⋆ᵐᵒᵈ(A, Π i, E i)
where
inner x y := ∑ i, ⟪x i, y i⟫_A
inner_add_right {x y z} := by simp [sum_add_distrib]
inner_self_nonneg := sum_nonneg <| fun _ _ ↦ CStarModule.inner_self_nonneg
inner_self
{x} := by
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
ext i
refine inner_self.mp <| le_antisymm (le_of_le_of_eq ?_ h) inner_self_nonneg
exact single_le_sum (fun i _ ↦ CStarModule.inner_self_nonneg (A := A) (x := x i)) (mem_univ _)
inner_op_smul_right := by simp [mul_sum]
inner_smul_right_complex := by simp [smul_sum]
star_inner x y := by simp
norm_eq_sqrt_norm_inner_self {x} := by with_reducible_and_instances rfl
