Subspaces of inner product spaces

This file defines the inner-product structure on a subspace of an inner-product space, and proves some theorems about orthogonal families of subspaces.

Inner product space structure on subspaces

instance Submodule.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (W : Submodule 𝕜 E) : InnerProductSpace 𝕜 ↥W

Induced inner product on a submodule.

Equations

• W.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Submodule.coe_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (W : Submodule 𝕜 E) (x y : ↥W) : inner x y = inner ↑x ↑y

The inner product on submodules is the same as on the ambient space.

theorem Orthonormal.codRestrict {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (s : Submodule 𝕜 E) (hvs : ∀ (i : ι), v i ∈ s) : Orthonormal 𝕜 (Set.codRestrict v (↑s) hvs)

theorem orthonormal_span {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : Orthonormal 𝕜 fun (i : ι) => ⟨v i, ⋯⟩

Families of mutually-orthogonal subspaces of an inner product space

def OrthogonalFamily (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (G : ι → Type u_5) [(i : ι) → SeminormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (V : (i : ι) → G i →ₗᵢ[𝕜] E) : Prop

An indexed family of mutually-orthogonal subspaces of an inner product space E.

The simple way to express this concept would be as a condition on V : ι → Submodule 𝕜 E. We instead implement it as a condition on a family of inner product spaces each equipped with an isometric embedding into E, thus making it a property of morphisms rather than subobjects. The connection to the subobject spelling is shown in orthogonalFamily_iff_pairwise.

This definition is less lightweight, but allows for better definitional properties when the inner product space structure on each of the submodules is important -- for example, when considering their Hilbert sum (PiLp V 2). For example, given an orthonormal set of vectors v : ι → E, we have an associated orthogonal family of one-dimensional subspaces of E, which it is convenient to be able to discuss using ι → 𝕜 rather than Π i : ι, span 𝕜 (v i).

Equations

• OrthogonalFamily 𝕜 G V = Pairwise fun (i j : ι) => ∀ (v : G i) (w : G j), inner ((V i) v) ((V j) w) = 0

theorem Orthonormal.orthogonalFamily {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : OrthogonalFamily 𝕜 (fun (_i : ι) => 𝕜) fun (i : ι) => LinearIsometry.toSpanSingleton 𝕜 E ⋯

theorem OrthogonalFamily.eq_ite {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [DecidableEq ι] {i j : ι} (v : G i) (w : G j) : inner ((V i) v) ((V j) w) = if i = j then inner ((V i) v) ((V j) w) else 0

theorem OrthogonalFamily.inner_right_dfinsupp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [(i : ι) → (x : G i) → Decidable (x ≠ 0)] [DecidableEq ι] (l : DirectSum ι fun (i : ι) => G i) (i : ι) (v : G i) : inner ((V i) v) (DFinsupp.sum l fun (j : ι) => ⇑(V j)) = inner v (l i)

theorem OrthogonalFamily.inner_right_fintype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [Fintype ι] (l : (i : ι) → G i) (i : ι) (v : G i) : inner ((V i) v) (∑ j : ι, (V j) (l j)) = inner v (l i)

theorem OrthogonalFamily.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (l₁ l₂ : (i : ι) → G i) (s : Finset ι) : inner (∑ i ∈ s, (V i) (l₁ i)) (∑ j ∈ s, (V j) (l₂ j)) = ∑ i ∈ s, inner (l₁ i) (l₂ i)

theorem OrthogonalFamily.norm_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (l : (i : ι) → G i) (s : Finset ι) : ‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2

theorem OrthogonalFamily.comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) {γ : Type u_6} {f : γ → ι} (hf : Function.Injective f) : OrthogonalFamily 𝕜 (fun (g : γ) => G (f g)) fun (g : γ) => V (f g)

The composition of an orthogonal family of subspaces with an injective function is also an orthogonal family.

theorem OrthogonalFamily.orthonormal_sigma_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) {α : ι → Type u_6} {v_family : (i : ι) → α i → G i} (hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)) : Orthonormal 𝕜 fun (a : (i : ι) × α i) => (V a.fst) (v_family a.fst a.snd)

theorem OrthogonalFamily.norm_sq_diff_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [DecidableEq ι] (f : (i : ι) → G i) (s₁ s₂ : Finset ι) : ‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2

theorem OrthogonalFamily.summable_iff_norm_sq_summable {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [CompleteSpace E] (f : (i : ι) → G i) : (Summable fun (i : ι) => (V i) (f i)) ↔ Summable fun (i : ι) => ‖f i‖ ^ 2

A family f of mutually-orthogonal elements of E is summable, if and only if (fun i ↦ ‖f i‖ ^ 2) is summable.

theorem OrthogonalFamily.independent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : iSupIndep V

An orthogonal family forms an independent family of subspaces; that is, any collection of elements each from a different subspace in the family is linearly independent. In particular, the pairwise intersections of elements of the family are 0.

theorem DirectSum.IsInternal.collectedBasis_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (hV_sum : DirectSum.IsInternal fun (i : ι) => V i) {α : ι → Type u_6} {v_family : (i : ι) → Basis (α i) 𝕜 ↥(V i)} (hv_family : ∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i)) : Orthonormal 𝕜 ⇑(hV_sum.collectedBasis v_family)