Extension by zero

noncomputable def Orthogonalization.MvN.extByZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y : ↥L →L[ℂ] ↥L) : H →L[ℂ] H

The extension by zero B(L) → B(H), y ↦ ι ∘ y ∘ π.

Equations

• Orthogonalization.MvN.extByZero L y = L.subtypeL ∘SL y ∘SL L.orthogonalProjectionOnto

theorem Orthogonalization.MvN.extByZero_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y : ↥L →L[ℂ] ↥L) (v : H) : (extByZero L y) v = ↑(y (L.orthogonalProjectionOnto v))

noncomputable def Orthogonalization.MvN.extByZeroₗ {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (L : Submodule ℂ H) [CompleteSpace ↥L] : (↥L →L[ℂ] ↥L) →ₗ[ℂ] H →L[ℂ] H

Extension by zero as a linear map.

Equations

• Orthogonalization.MvN.extByZeroₗ L = { toFun := Orthogonalization.MvN.extByZero L, map_add' := ⋯, map_smul' := ⋯ }

theorem Orthogonalization.MvN.extByZeroₗ_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y : ↥L →L[ℂ] ↥L) : (extByZeroₗ L) y = extByZero L y

theorem Orthogonalization.MvN.extByZero_sum {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] {κ : Type u_1} (s : Finset κ) (f : κ → ↥L →L[ℂ] ↥L) : extByZero L (∑ k ∈ s, f k) = ∑ k ∈ s, extByZero L (f k)

theorem Orthogonalization.MvN.extByZero_sub {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y z : ↥L →L[ℂ] ↥L) : extByZero L (y - z) = extByZero L y - extByZero L z

theorem Orthogonalization.MvN.compressTo_extByZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y : ↥L →L[ℂ] ↥L) : CommutingRepetition.VN.compressTo L (extByZero L y) = y

theorem Orthogonalization.MvN.extByZero_compressTo {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] {x : H →L[ℂ] H} (hx : L.starProjection * x * L.starProjection = x) : extByZero L (CommutingRepetition.VN.compressTo L x) = x

theorem Orthogonalization.MvN.extByZero_mul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y z : ↥L →L[ℂ] ↥L) : extByZero L (y * z) = extByZero L y * extByZero L z

theorem Orthogonalization.MvN.extByZero_star {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y : ↥L →L[ℂ] ↥L) : extByZero L (star y) = star (extByZero L y)

theorem Orthogonalization.MvN.extByZero_one {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] : extByZero L 1 = L.starProjection

theorem Orthogonalization.MvN.extByZero_mul_starProjection {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] (y : ↥L →L[ℂ] ↥L) : extByZero L y * L.starProjection = extByZero L y

noncomputable def Orthogonalization.MvN.compressToₗ' {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] : (H →L[ℂ] H) →ₗ[ℂ] ↥L →L[ℂ] ↥L

The compression as a linear map (general H).

Equations

• Orthogonalization.MvN.compressToₗ' L = { toFun := CommutingRepetition.VN.compressTo L, map_add' := ⋯, map_smul' := ⋯ }

theorem Orthogonalization.MvN.compressTo_sum' {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] {κ : Type u_1} (s : Finset κ) (f : κ → H →L[ℂ] H) : CommutingRepetition.VN.compressTo L (∑ k ∈ s, f k) = ∑ k ∈ s, CommutingRepetition.VN.compressTo L (f k)

theorem Orthogonalization.MvN.compressTo_nonneg' {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] {T : H →L[ℂ] H} (hT : 0 ≤ T) : 0 ≤ CommutingRepetition.VN.compressTo L T

theorem Orthogonalization.MvN.compressTo_starProjection_self {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (L : Submodule ℂ H) [CompleteSpace ↥L] : CommutingRepetition.VN.compressTo L L.starProjection = 1

Theorem 1.2 at a finite-rank projection of B(H)

theorem Orthogonalization.MvN.orthAtP_of_mem_all_finiteRank {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hM : ∀ (x : H →L[ℂ] H), x ∈ M) (L : Submodule ℂ H) [FiniteDimensional ℂ ↥L] (ι : Type u_1) [Fintype ι] (P : ((H →L[ℂ] H) →ₗ[ℂ] ℂ) → Prop) : Blocks.OrthAtP M L.starProjection ι P

For a von Neumann algebra containing every operator and a finite-dimensional subspace L, Theorem 1.2 holds at the projection onto L (for every class of functionals): the corner is B(L) and the T1a engine applies.

The net of finite-rank projections

theorem Orthogonalization.MvN.orthAtN_of_mem_all {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hM : ∀ (x : H →L[ℂ] H), x ∈ M) (ι : Type u_1) [Fintype ι] : OrthAtN M 1 ι

Theorem 1.2 for a von Neumann algebra containing every operator, for normal functionals, on an arbitrary Hilbert space.

theorem Orthogonalization.povm_orthogonalization_of_mem_all_general {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hM : ∀ (x : H →L[ℂ] H), x ∈ M) (φ : NormalState M) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : IsPOVM M a) (ε : ℝ) (hε : 1 - ε < (φ.toLinearMap (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), IsPVM M p ∧ (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 (povm_orthogonalization) for a von Neumann algebra containing every operator of an arbitrary Hilbert space H: the instance of the signed statement delivered by tier T2.

theorem Orthogonalization.povm_orthogonalization_fullAlgebra_general {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (φ : NormalState (fullAlgebra H)) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : IsPOVM (fullAlgebra H) a) (ε : ℝ) (hε : 1 - ε < (φ.toLinearMap (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), IsPVM (fullAlgebra H) p ∧ (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 (povm_orthogonalization) for M = B(H), H an arbitrary Hilbert space (tier T2).