TensorSlices.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Vanishing tensor slices in the propagation argument

A bounded weakly null family of vectors gives strongly vanishing slices of any fixed vector in the completed Hilbert tensor product. This is the density step in lem:propagation, with the uniform bound proved on the completion.

theorem OAI.KadisonSimilarity.orthonormal_inner_tendsto_zero line 27

Source documentation

Bessel's inequality makes every orthonormal sequence weakly null.

theorem orthonormal_inner_tendsto_zero (x : ℕ → E) (hx : Orthonormal ℂ x) (a : E) :
    Tendsto (fun n => inner ℂ (x n) a) atTop (𝓝 0) := by
…

def OAI.KadisonSimilarity.HilbertTensor line 35

Source documentation

The Hilbert completion of the algebraic tensor product.

def HilbertTensor (E F : Type*) [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] :=
…

instance OAI.KadisonSimilarity.hilbertTensorNormedAddCommGroup line 42
Source documentation
Keep the canonical completed-tensor structures named. In iterated word spaces this shares the structure terms instead of expanding each completion and algebraic tensor instance at every use.
```
instance hilbertTensorNormedAddCommGroup : NormedAddCommGroup (HilbertTensor E F) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
instance OAI.KadisonSimilarity.hilbertTensorInnerProductSpace line 46
instance OAI.KadisonSimilarity.hilbertTensorCompleteSpace line 50
instance OAI.KadisonSimilarity.hilbertTensorCoe line 54
theorem OAI.KadisonSimilarity.norm_hilbertTensor_coe line 57
def OAI.KadisonSimilarity.algebraTensorSlice line 62
Source documentation
Contract the first tensor coordinate against x.
```
def algebraTensorSlice (x : E) : E ⊗[ℂ] F →L[ℂ] F :=
…
```
theorem OAI.KadisonSimilarity.algebraTensorSlice_tmul line 66
theorem OAI.KadisonSimilarity.norm_algebraTensorSlice_apply_le line 70
def OAI.KadisonSimilarity.tensorSlice line 91
Source documentation
The slice extends uniquely to the completed Hilbert tensor product.
```
def tensorSlice (x : E) : HilbertTensor E F →L[ℂ] F :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.tensorSlice_coe line 94
theorem OAI.KadisonSimilarity.norm_tensorSlice_apply_le line 98

theorem OAI.KadisonSimilarity.algebraTensorSlice_tendsto_zero line 110

Source documentation

First prove convergence on finite tensor sums, before taking completion.

theorem algebraTensorSlice_tendsto_zero (x : ℕ → E)
    (hweak : ∀ a : E, Tendsto (fun n => inner ℂ (x n) a) atTop (𝓝 0))
    (z : E ⊗[ℂ] F) :
    Tendsto (fun n => algebraTensorSlice (x n) z) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonSimilarity.algebraTensorSlice

theorem OAI.KadisonSimilarity.tensorSlice_tendsto_zero line 120
Source documentation
Weak convergence in the first factor yields norm convergence of each fixed tensor slice. No uniform rate over tensor vectors is asserted.
```
theorem tensorSlice_tendsto_zero (x : ℕ → E)
    (hbound : ∀ n, ‖x n‖ ≤ 1)
    (hweak : ∀ a : E, Tendsto (fun n => inner ℂ (x n) a) atTop (𝓝 0))
    (z : HilbertTensor E F) :
    Tendsto (fun n => tensorSlice (x n) z) atTop (𝓝 0) := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.tensorSlice
theorem OAI.KadisonSimilarity.tensorSlice_tendsto_zero_of_orthonormal line 152
Source documentation
In particular the normalized Haar powers used in propagation give vanishing slices once their orthonormality has been established.
```
theorem tensorSlice_tendsto_zero_of_orthonormal (x : ℕ → E) (hx : Orthonormal ℂ x)
    (z : HilbertTensor E F) :
    Tendsto (fun n => tensorSlice (x n) z) atTop (𝓝 0) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.tensorSlice