Completion of an inner product space

We show that the separation quotient and the completion of an inner product space are inner product spaces.

theorem Inseparable.inner_eq_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x₁ x₂ y₁ y₂ : E} (hx : Inseparable x₁ x₂) (hy : Inseparable y₁ y₂) : inner x₁ y₁ = inner x₂ y₂

instance SeparationQuotient.instInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Inner 𝕜 (SeparationQuotient E)

Equations

• SeparationQuotient.instInner = { inner := SeparationQuotient.lift₂ inner ⋯ }

@[simp]

theorem SeparationQuotient.inner_mk_mk {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : inner (SeparationQuotient.mk x) (SeparationQuotient.mk y) = inner x y

instance SeparationQuotient.instInnerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 (SeparationQuotient E)

Equations

• SeparationQuotient.instInnerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

instance UniformSpace.Completion.toInner {𝕜' : Type u_4} {E' : Type u_5} [TopologicalSpace 𝕜'] [UniformSpace E'] [Inner 𝕜' E'] : Inner 𝕜' (UniformSpace.Completion E')

Equations

• UniformSpace.Completion.toInner = { inner := Function.curry (⋯.extend (Function.uncurry inner)) }

@[simp]

theorem UniformSpace.Completion.inner_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (a b : E) : inner (↑E a) (↑E b) = inner a b

theorem UniformSpace.Completion.continuous_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Continuous (Function.uncurry inner)

theorem UniformSpace.Completion.Continuous.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → UniformSpace.Completion E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => inner (f x) (g x)

instance UniformSpace.Completion.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 (UniformSpace.Completion E)

Equations

• UniformSpace.Completion.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯