TensorHeadSlices.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Vacuum coefficients of a head tensor action

The exceptional-projection formula in propagation follows from the actual head action on the completed tensor product. It does not need to be assumed separately for every vector or every term of the Haar sequence.

theorem OAI.KadisonSimilarity.hilbertTensorInsert_adjoint line 25
Source documentation
The adjoint of endpoint insertion is the completed tensor slice.
```
theorem hilbertTensorInsert_adjoint (Ω : E) :
    (hilbertTensorInsert (H := F) Ω).adjoint = tensorSlice Ω := by
…
```
Mentions: OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tensorSlice
def OAI.KadisonSimilarity.vacuumSubspace line 34
Source documentation
The actual vacuum subspace in a completed head-tail tensor product.
```
def vacuumSubspace (Ω : E) : Submodule ℂ (HilbertTensor E F) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.vacuum_remainder_orthogonal line 38
Source documentation
Subtracting the vacuum coefficient leaves an orthogonal vector.
```
theorem vacuum_remainder_orthogonal (Ω : E) (hΩ : ‖Ω‖ = 1) (z : HilbertTensor E F) :
    z - hilbertTensorInsert Ω (tensorSlice Ω z) ∈ (vacuumSubspace (F := F) Ω)ᗮ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tensorSlice, OAI.KadisonSimilarity.vacuumSubspace
theorem OAI.KadisonSimilarity.vacuumSubspace_hasOrthogonalProjection line 56
Source documentation
The vacuum projection exists directly from the tensor decomposition.
```
theorem vacuumSubspace_hasOrthogonalProjection (Ω : E) (hΩ : ‖Ω‖ = 1) :
    (vacuumSubspace (F := F) Ω).HasOrthogonalProjection where
…
```
Mentions: OAI.KadisonSimilarity.vacuumSubspace
theorem OAI.KadisonSimilarity.vacuumSubspace_starProjection line 63
Source documentation
The orthogonal projection onto the vacuum subspace is insertion followed by its adjoint.
```
theorem vacuumSubspace_starProjection (Ω : E) (hΩ : ‖Ω‖ = 1)
    [(vacuumSubspace (F := F) Ω).HasOrthogonalProjection] :
…
```
Mentions: OAI.KadisonSimilarity.vacuumSubspace
def OAI.KadisonSimilarity.tensorHeadAction line 75
Source documentation
Act on the head factor while leaving the completed tail unchanged.
```
def tensorHeadAction (X : E →L[ℂ] E) : HilbertTensor E F →L[ℂ] HilbertTensor E F :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.tensorHeadAction_insert line 79
theorem OAI.KadisonSimilarity.tensorSlice_head line 90
Source documentation
Moving the head operator to the slicing vector takes its adjoint.
```
theorem tensorSlice_head (Ω : E) (X : E →L[ℂ] E) :
    (tensorSlice (F := F) Ω).comp (tensorHeadAction X) = tensorSlice (X.adjoint Ω) := by
…
```
Mentions: OAI.KadisonSimilarity.tensorSlice, OAI.KadisonSimilarity.tensorHeadAction
theorem OAI.KadisonSimilarity.firstLetterProjection_head line 99
Source documentation
The full vacuum projection after multiplication is the slice against X*Ω, followed by insertion of Ω.
```
theorem firstLetterProjection_head (Ω : E) (X : E →L[ℂ] E) :
    (firstLetterProjection Ω (ContinuousLinearMap.id ℂ F)).comp (tensorHeadAction X) =
      (hilbertTensorInsert Ω).comp (tensorSlice (X.adjoint Ω)) := by
…
```
Mentions: OAI.KadisonSimilarity.firstLetterProjection, OAI.KadisonSimilarity.tensorHeadAction, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tensorSlice
theorem OAI.KadisonSimilarity.firstLetterProjection_head_tendsto_zero line 107
Source documentation
In particular the actual head action of an orthonormal adjoint-vector sequence has vanishing vacuum coefficient on every fixed tensor.
```
theorem firstLetterProjection_head_tendsto_zero (Ω : E) (X : ℕ → E →L[ℂ] E)
    (hX : Orthonormal ℂ (fun n => (X n).adjoint Ω)) (z : HilbertTensor E F) :
    Filter.Tendsto (fun n => firstLetterProjection Ω (ContinuousLinearMap.id ℂ F)
      (tensorHeadAction (X n) z)) Filter.atTop (nhds 0) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.firstLetterProjection, OAI.KadisonSimilarity.tensorHeadAction
abbrev OAI.KadisonSimilarity.tracialVacuumSubspace line 124
Source documentation
Transport the actual vacuum subspace through tracial word coordinates.
```
abbrev tracialVacuumSubspace (U : H ≃ₗᵢ[ℂ] HilbertTensor E F) (Ω : E) : Submodule ℂ H :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.tracialVacuumSubspace_hasOrthogonalProjection line 129
Source documentation
The transported vacuum subspace also has its orthogonal projection.
```
theorem tracialVacuumSubspace_hasOrthogonalProjection
    (U : H ≃ₗᵢ[ℂ] HilbertTensor E F) (Ω : E) (hΩ : ‖Ω‖ = 1) :
    (tracialVacuumSubspace U Ω).HasOrthogonalProjection := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.tracialVacuumSubspace
theorem OAI.KadisonSimilarity.tracialVacuumSubspace_projection_coordinates line 139
Source documentation
The projection-coordinate identity follows from its actual subspace construction, rather than being additional word-model data.
```
theorem tracialVacuumSubspace_projection_coordinates
    (U : H ≃ₗᵢ[ℂ] HilbertTensor E F) (Ω : E) (hΩ : ‖Ω‖ = 1)
    [(vacuumSubspace (F := F) Ω).HasOrthogonalProjection]
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.vacuumSubspace

theorem OAI.KadisonSimilarity.vacuum_slice_in_coordinates line 153

Source documentation

Transport the head-action formula to a tracial word realization. The two hypotheses are the ordinary coordinate identities for multiplication and for the vacuum projection.

theorem vacuum_slice_in_coordinates
    (U : H ≃ₗᵢ[ℂ] HilbertTensor E F) (Ω : E)
    (P : Submodule ℂ H) [P.HasOrthogonalProjection]
    (X : H →L[ℂ] H) (T : E →L[ℂ] E)
    (hP : ∀ z, U (P.starProjection z) =
      firstLetterProjection Ω (ContinuousLinearMap.id ℂ F) (U z))
    (hX : ∀ z, U (X z) = tensorHeadAction T (U z)) (z : H) :
    P.starProjection (X z) = U.symm
      (hilbertTensorInsert Ω (tensorSlice (T.adjoint Ω) (U z))) := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.firstLetterProjection, OAI.KadisonSimilarity.tensorHeadAction, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tensorSlice

theorem OAI.KadisonSimilarity.vacuum_projection_tendsto_zero_of_head_coordinates line 169

Source documentation

Thus the vanishing projection required for propagation follows directly from the head-action representation and orthonormality of the adjoint letters.

theorem vacuum_projection_tendsto_zero_of_head_coordinates
    (U : H ≃ₗᵢ[ℂ] HilbertTensor E F) (Ω : E)
    (P : Submodule ℂ H) [P.HasOrthogonalProjection]
    (X : ℕ → H →L[ℂ] H) (T : ℕ → E →L[ℂ] E)
    (hP : ∀ z, U (P.starProjection z) =
      firstLetterProjection Ω (ContinuousLinearMap.id ℂ F) (U z))
    (hX : ∀ n z, U (X n z) = tensorHeadAction (T n) (U z))
    (horth : Orthonormal ℂ (fun n => (T n).adjoint Ω)) (z : H) :
    Filter.Tendsto (fun n => P.starProjection (X n z)) Filter.atTop (nhds 0) := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.firstLetterProjection, OAI.KadisonSimilarity.tensorHeadAction