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_reducible]

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 𝕜 (mk x) (mk y) = inner 𝕜 x y

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance UniformSpace.Completion.toInner {𝕜' : Type u_3} {E' : Type u_4} [TopologicalSpace 𝕜'] [UniformSpace E'] [Inner 𝕜' E'] : Inner 𝕜' (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 𝕜 ↑a ↑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_3} [TopologicalSpace α] {f g : α → Completion E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => inner 𝕜 (f x) (g x)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.