instance PiLp.innerProductSpace' {𝕜 : Type u_1} {ι : Type u_2} [AddCommMonoid 𝕜] [Fintype ι] {α : ι → Type u_3} [(i : ι) → Inner 𝕜 (α i)] : Inner 𝕜 (PiLp 2 α)

Equations

• PiLp.innerProductSpace' = { inner := fun (x y : PiLp 2 α) => Finset.sum Finset.univ fun (i : ι) => ⟪x i, y i⟫_𝕜 }

@[simp]

theorem PiLp.inner_apply' {𝕜 : Type u_1} {ι : Type u_2} [AddCommMonoid 𝕜] [Fintype ι] {α : ι → Type u_3} [(i : ι) → Inner 𝕜 (α i)] (x : PiLp 2 α) (y : PiLp 2 α) : ⟪x, y⟫_𝕜 = Finset.sum Finset.univ fun (i : ι) => ⟪x i, y i⟫_𝕜