MIPRE.Background.Orthonormalization.Orthogonalization.FinDim.Blocks

source

@[reducible, inline]

abbrev Orthogonalization.FinDim.BlockSpace (H : Type u_1) (ι : Type u_2) :

Type (max u_1 u_2)

The Hilbert space direct sum H^ι.

Equations

Orthogonalization.FinDim.BlockSpace H ι = PiLp 2 fun (x : ι) => H

Instances For

source

theorem Orthogonalization.FinDim.sumA {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {κ : Type u_3} (s : Finset κ) (f : κ → BlockSpace H ι) (j : ι) :

(∑ k ∈ s, f k).ofLp j = ∑ k ∈ s, (f k).ofLp j

Evaluating a finite sum of block vectors coordinatewise.

source

theorem Orthogonalization.FinDim.sumCLM {κ : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℂ E] [NormedSpace ℂ F] (s : Finset κ) (f : κ → E →L[ℂ ] F) (v : E) :

(∑ k ∈ s, f k) v = ∑ k ∈ s, (f k) v

Applying a finite sum of operators.

source

noncomputable def Orthogonalization.FinDim.embed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [DecidableEq ι] (i : ι) :

H →L[ℂ ] BlockSpace H ι

Coordinate embedding v ↦ (0, …, v, …, 0).

Equations

Orthogonalization.FinDim.embed i = ↑(PiLp.continuousLinearEquiv 2 ℂ fun (x : ι) => H).symm ∘SL ContinuousLinearMap.pi fun (j : ι) => if j = i then ContinuousLinearMap.id ℂ H else 0

Instances For

source

noncomputable def Orthogonalization.FinDim.proj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} (i : ι) :

BlockSpace H ι →L[ℂ ] H

Coordinate projection.

Equations

Orthogonalization.FinDim.proj i = PiLp.proj 2 (fun (x : ι) => H) i

Instances For

source

theorem Orthogonalization.FinDim.embed_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i j : ι) (v : H) :

((embed i) v).ofLp j = if j = i then v else 0

source

theorem Orthogonalization.FinDim.proj_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (w : BlockSpace H ι) :

(proj i) w = w.ofLp i

source

theorem Orthogonalization.FinDim.proj_embed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i j : ι) (v : H) :

(proj i) ((embed j) v) = if i = j then v else 0

source

theorem Orthogonalization.FinDim.proj_embed_same {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (v : H) :

(proj i) ((embed i) v) = v

source

theorem Orthogonalization.FinDim.proj_embed_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {i j : ι} (h : i ≠ j) (v : H) :

(proj i) ((embed j) v) = 0

source

theorem Orthogonalization.FinDim.sum_embed_proj_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (w : BlockSpace H ι) :

∑ i : ι, (embed i) ((proj i) w) = w

source

theorem Orthogonalization.FinDim.inner_embed_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) (v : H) (w : BlockSpace H ι) :

inner ℂ ((embed i) v) w = inner ℂ v (w.ofLp i)

source

theorem Orthogonalization.FinDim.adjoint_embed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) :

ContinuousLinearMap.adjoint (embed i) = proj i

source

theorem Orthogonalization.FinDim.adjoint_proj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) :

ContinuousLinearMap.adjoint (proj i) = embed i

source

noncomputable def Orthogonalization.FinDim.blockMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (X : ι → H →L[ℂ ] H) :

H →L[ℂ ] BlockSpace H ι

The map T = ∑ embed i ∘ X i : H → H^ι with blocks X i.

Equations

Orthogonalization.FinDim.blockMap X = ∑ i : ι, Orthogonalization.FinDim.embed i ∘SL X i

Instances For

source

theorem Orthogonalization.FinDim.blockMap_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (X : ι → H →L[ℂ ] H) (v : H) :

(blockMap X) v = ∑ i : ι, (embed i) ((X i) v)

source

theorem Orthogonalization.FinDim.proj_blockMap_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (X : ι → H →L[ℂ ] H) (i : ι) (v : H) :

(proj i) ((blockMap X) v) = (X i) v

source

theorem Orthogonalization.FinDim.proj_comp_blockMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (X : ι → H →L[ℂ ] H) (i : ι) :

proj i ∘SL blockMap X = X i

source

noncomputable def Orthogonalization.FinDim.blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ι → H →L[ℂ ] H) :

BlockSpace H ι →L[ℂ ] BlockSpace H ι

The block projection Q = ∑ embed i ∘ q i ∘ proj i on H^ι.

Equations

Orthogonalization.FinDim.blockProj q = ∑ i : ι, Orthogonalization.FinDim.embed i ∘SL q i ∘SL Orthogonalization.FinDim.proj i

Instances For

source

theorem Orthogonalization.FinDim.blockProj_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ι → H →L[ℂ ] H) (w : BlockSpace H ι) :

(blockProj q) w = ∑ i : ι, (embed i) ((q i) (w.ofLp i))

source

theorem Orthogonalization.FinDim.blockProj_apply_coord {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ι → H →L[ℂ ] H) (w : BlockSpace H ι) (j : ι) :

((blockProj q) w).ofLp j = (q j) (w.ofLp j)

source

theorem Orthogonalization.FinDim.proj_blockProj_embed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ι → H →L[ℂ ] H) (i j : ι) (v : H) :

(proj i) ((blockProj q) ((embed j) v)) = if i = j then (q i) v else 0

source

theorem Orthogonalization.FinDim.blockProj_blockMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q X : ι → H →L[ℂ ] H) (v : H) :

(blockProj q) ((blockMap X) v) = (blockMap fun (i : ι) => q i ∘SL X i) v