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_3} {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_3} [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_3} [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_3} [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_3} [TopologicalSpace α] {f g : α → E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (t : α) => Inner.inner 𝕜 (f t) (g t)

theorem Dense.eq_zero_of_inner_left {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 x v = 0) : x = 0

theorem Dense.eq_zero_of_inner_right {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 v x = 0) : x = 0

theorem Dense.eq_of_inner_left {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 x v = inner 𝕜 y v) : x = y

theorem Dense.eq_of_inner_right {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 v x = inner 𝕜 v y) : x = y

theorem DenseRange.eq_of_inner_left {E : Type u_3} {ι : Type u_4} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} {f : ι → E} (hf : DenseRange f) (h : ∀ (i : ι), inner 𝕜 x (f i) = inner 𝕜 y (f i)) : x = y

theorem DenseRange.eq_of_inner_right {E : Type u_3} {ι : Type u_4} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} {f : ι → E} (hf : DenseRange f) (h : ∀ (i : ι), inner 𝕜 (f i) x = inner 𝕜 (f i) y) : x = y

theorem DenseRange.eq_zero_of_inner_left {E : Type u_3} {ι : Type u_4} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {f : ι → E} (hf : DenseRange f) (h : ∀ (i : ι), inner 𝕜 x (f i) = 0) : x = 0

theorem DenseRange.eq_zero_of_inner_right {E : Type u_3} {ι : Type u_4} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {f : ι → E} (hf : DenseRange f) (h : ∀ (i : ι), inner 𝕜 (f i) x = 0) : x = 0