Continuity of inner product

We show that the inner product is continuous, continuous_inner.

Tags

inner product space, Hilbert space, norm

Continuity of the inner product

theorem isBoundedBilinearMap_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] : IsBoundedBilinearMap ℝ fun (p : E × E) => inner p.1 p.2

When an inner product space E over 𝕜 is considered as a real normed space, its inner product satisfies IsBoundedBilinearMap.

In order to state these results, we need a NormedSpace ℝ E instance. We will later establish such an instance by restriction-of-scalars, InnerProductSpace.rclikeToReal 𝕜 E, but this instance may be not definitionally equal to some other “natural” instance. So, we assume [NormedSpace ℝ E].

theorem continuous_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Continuous fun (p : E × E) => inner p.1 p.2

theorem Filter.Tendsto.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} {f g : α → E} {l : Filter α} {x y : E} (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) : Tendsto (fun (t : α) => Inner.inner (f t) (g t)) l (nhds (Inner.inner x y))

theorem ContinuousWithinAt.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → E} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (t : α) => Inner.inner (f t) (g t)) s x

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

theorem ContinuousOn.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → E} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (t : α) => Inner.inner (f t) (g t)) s

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