EndpointTensors.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Completed tensor words with an unrestricted first endpoint

The endpoint and the centered tail may live in different Hilbert spaces. Their completed tensor product has total elementary words and carries the operators I ⊗ A and endpoint slices.

theorem OAI.KadisonSimilarity.inner_hilbertTensor_coe line 23
theorem OAI.KadisonSimilarity.hilbertTensor_coe_add line 27

abbrev OAI.KadisonSimilarity.EndpointTensor line 33

Source documentation

An unrestricted endpoint followed by a completed centered tail.

abbrev EndpointTensor (E F : Type*) [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] (n : ℕ) :=
…

def OAI.KadisonSimilarity.endpointInsert line 38
Source documentation
Insert an endpoint in front of a completed tail vector.
```
def endpointInsert {n : ℕ} (d : E) :
    CompletedTensorWord F n →L[ℂ] EndpointTensor E F n :=
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor
def OAI.KadisonSimilarity.endpointWord line 43
Source documentation
The elementary word with an unrestricted first endpoint.
```
def endpointWord {n : ℕ} (d : E) (x : Fin n → F) : EndpointTensor E F n :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor
theorem OAI.KadisonSimilarity.endpointInsert_apply line 46
theorem OAI.KadisonSimilarity.norm_endpointInsert line 49
theorem OAI.KadisonSimilarity.norm_endpointInsert_le line 54
theorem OAI.KadisonSimilarity.inner_endpointInsert line 60
theorem OAI.KadisonSimilarity.inner_endpointWord line 66

theorem OAI.KadisonSimilarity.endpointWord_mem_closed_submodule line 72

Source documentation

Endpoint words are total in the completed endpoint tensor product.

theorem endpointWord_mem_closed_submodule {n : ℕ}
    (S : Submodule ℂ (EndpointTensor E F n)) (hclosed : IsClosed (S : Set (EndpointTensor E F n)))
    (hword : ∀ d x, endpointWord d x ∈ S) (z : EndpointTensor E F n) : z ∈ S := by
…

Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.endpointWord

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_endpointWords line 90
Source documentation
Continuous linear maps on endpoint words are determined by elementary words.
```
theorem continuousLinearMap_ext_endpointWords {G : Type*}
    [NormedAddCommGroup G] [NormedSpace ℂ G] {n : ℕ}
    (f g : EndpointTensor E F n →L[ℂ] G)
    (hword : ∀ d x, f (endpointWord d x) = g (endpointWord d x)) : f = g := by
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.endpointWord
theorem OAI.KadisonSimilarity.endpointOperator_eq_zero_of_word_coefficients line 103
Source documentation
Vanishing matrix coefficients on all endpoint words force the operator to vanish.
```
theorem endpointOperator_eq_zero_of_word_coefficients {k l : ℕ}
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l)
    (hword : ∀ d x c z, inner ℂ (endpointWord c z) (Y (endpointWord d x)) = 0) : Y = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.endpointWord
def OAI.KadisonSimilarity.endpointTensorMap line 125
Source documentation
The completed tensor product of an endpoint map and a bounded tail operator.
```
def endpointTensorMap {k l : ℕ} (p : E →L[ℂ] E')
    (A : CompletedTensorWord F k →L[ℂ] CompletedTensorWord F' l) :
    EndpointTensor E F k →L[ℂ] EndpointTensor E' F' l :=
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor
theorem OAI.KadisonSimilarity.endpointTensorMap_insert line 130
def OAI.KadisonSimilarity.endpointAmplification line 142
Source documentation
The actual operator I_E ⊗ A on completed endpoint tensors.
```
def endpointAmplification {k l : ℕ}
    (A : CompletedTensorWord F k →L[ℂ] CompletedTensorWord F l) :
    EndpointTensor E F k →L[ℂ] EndpointTensor E F l :=
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor
theorem OAI.KadisonSimilarity.endpointAmplification_insert line 147
theorem OAI.KadisonSimilarity.inner_tensorSlice_endpointInsert line 154
Source documentation
Contracting the endpoint is adjoint to inserting that endpoint.
```
theorem inner_tensorSlice_endpointInsert {n : ℕ} (d : E)
    (x : CompletedTensorWord F n) (z : EndpointTensor E F n) :
    inner ℂ x (tensorSlice d z) = inner ℂ (endpointInsert d x) z := by
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.tensorSlice, OAI.KadisonSimilarity.endpointInsert
def OAI.KadisonSimilarity.endpointCompression line 193
Source documentation
Compress the endpoint of a bounded operator to the chosen trace vector.
```
def endpointCompression {k l : ℕ} (Ω : E)
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l) :
    CompletedTensorWord F k →L[ℂ] CompletedTensorWord F l :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.CompletedTensorWord
theorem OAI.KadisonSimilarity.endpointCompression_coefficient line 198

theorem OAI.KadisonSimilarity.endpointOperator_eq_amplification line 207

Source documentation

Coefficient factorization reconstructs I_E ⊗ A using proved totality.

theorem endpointOperator_eq_amplification {k l : ℕ}
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l)
    (A : CompletedTensorWord F k →L[ℂ] CompletedTensorWord F l)
    (hcoeff : ∀ d x c z, inner ℂ (endpointWord c z) (Y (endpointWord d x)) =
      inner ℂ c d * inner ℂ (completedTensorWord z) (A (completedTensorWord x))) :
    Y = endpointAmplification A := by
…

Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.completedTensorWord, OAI.KadisonSimilarity.endpointAmplification

def OAI.KadisonSimilarity.endpointHeadAction line 222
Source documentation
A bounded operator acting only on the unrestricted endpoint.
```
def endpointHeadAction {n : ℕ} (p : E →L[ℂ] E) :
    EndpointTensor E F n →L[ℂ] EndpointTensor E F n :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor
theorem OAI.KadisonSimilarity.endpointHeadAction_insert line 226
theorem OAI.KadisonSimilarity.inner_endpointHeadAction line 235
Source documentation
Moving an endpoint action across an inner product requires only the ordinary Hilbert adjoint law.
```
theorem inner_endpointHeadAction {n : ℕ} (p : E →L[ℂ] E)
    (c : E) (z : CompletedTensorWord F n) (w : EndpointTensor E F n) :
    inner ℂ (endpointInsert c z) (endpointHeadAction p w) =
      inner ℂ (endpointInsert (p.adjoint c) z) w := by
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.endpointInsert, OAI.KadisonSimilarity.endpointHeadAction
theorem OAI.KadisonSimilarity.endpoint_coefficient_transfer line 251
Source documentation
Left intertwining moves arbitrary first endpoints to the trace-vector coefficient. This is the algebraic replacement for a separate commutant theorem.
```
theorem endpoint_coefficient_transfer {k l : ℕ}
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l) (p : E →L[ℂ] E)
    (hY : Y.comp (endpointHeadAction (n := k) p) =
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.endpointHeadAction
theorem OAI.KadisonSimilarity.norm_endpointWord_le_matrix_units line 269
Source documentation
An endpoint and n matrix-unit tail letters contribute n + 1 normalized Hilbert--Schmidt factors, even when endpoint and tail spaces differ.
```
theorem norm_endpointWord_le_matrix_units {n : ℕ} (d : E) (x : Fin n → F)
    (m : ℝ) (hm : 0 < m) (hd : ‖d‖ ≤ m ^ (-(1 : ℝ) / 2))
    (hx : ∀ i, ‖x i‖ ≤ m ^ (-(1 : ℝ) / 2)) :
    ‖endpointWord d x‖ ≤ m ^ (-((n : ℝ) + 1) / 2) := by
…
```
Mentions: OAI.KadisonSimilarity.endpointWord