TensorWords.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Finite words in completed Hilbert tensor powers

The scalar word has length zero. Longer words are genuine Hilbert tensor products, completed only after the finite algebraic tensor product is formed.

abbrev OAI.KadisonSimilarity.TensorScalars line 21
Source documentation
Scalars at the same universe as the Hilbert space.
```
abbrev TensorScalars : Type u := ULift.{u} ℂ
```
instance OAI.KadisonSimilarity.tensorScalarsInnerProductSpace line 23
structure OAI.KadisonSimilarity.TensorWordSpace line 33
Source documentation
Bundling keeps the vector-space structures available during the recursion.
```
structure TensorWordSpace where
…
```

def OAI.KadisonSimilarity.tensorWordSpace line 41

Source documentation

Right-associated algebraic Hilbert tensor powers, including degree zero.

def tensorWordSpace (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℂ E] :
    ℕ → TensorWordSpace.{u}
  | 0 => ⟨TensorScalars, inferInstance, inferInstance⟩
  | n + 1 => ⟨E ⊗[ℂ] (tensorWordSpace E n).Carrier, inferInstance, inferInstance⟩

Mentions: OAI.KadisonSimilarity.TensorScalars

abbrev OAI.KadisonSimilarity.TensorWord line 46

def OAI.KadisonSimilarity.tensorWord line 50

Source documentation

The elementary word determined by its letters.

def tensorWord : {n : ℕ} → (Fin n → E) → TensorWord E n
  | 0, _ => ⟨1⟩
  | _n + 1, x => x 0 ⊗ₜ[ℂ] tensorWord (Fin.tail x)

/-- Inner products of words are products of the inner products of letters. -/

Mentions: OAI.KadisonSimilarity.TensorWord

theorem OAI.KadisonSimilarity.inner_tensorWord line 55
Source documentation
Inner products of words are products of the inner products of letters.
```
theorem inner_tensorWord {n : ℕ} (x y : Fin n → E) :
    inner ℂ (tensorWord x) (tensorWord y) = ∏ i, inner ℂ (x i) (y i) := by
…
```
Mentions: OAI.KadisonSimilarity.tensorWord
abbrev OAI.KadisonSimilarity.CompletedTensorWord line 68
Source documentation
Completed finite Hilbert tensor powers.
```
abbrev CompletedTensorWord (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (n : ℕ) := UniformSpace.Completion (TensorWord E n)
```
Mentions: OAI.KadisonSimilarity.TensorWord
def OAI.KadisonSimilarity.completedTensorWord line 72
Source documentation
An elementary word in the completed tensor power.
```
def completedTensorWord {n : ℕ} (x : Fin n → E) : CompletedTensorWord E n := tensorWord x
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.tensorWord
theorem OAI.KadisonSimilarity.inner_completedTensorWord line 74
theorem OAI.KadisonSimilarity.orthonormal_completedTensorWords line 80
Source documentation
All words formed from an orthonormal alphabet form an orthonormal family.
```
theorem orthonormal_completedTensorWords {J : Type*} (h : J → E) (hh : Orthonormal ℂ h)
    (n : ℕ) :
    Orthonormal ℂ (fun f : Fin n → J => completedTensorWord (fun i => h (f i))) := by
…
```
Mentions: OAI.KadisonSimilarity.completedTensorWord
theorem OAI.KadisonSimilarity.norm_sum_orthonormal line 100
Source documentation
The sum of a finite orthonormal family has norm the square root of its cardinality. This supplies the exact growth rate in the pairing test.
```
theorem norm_sum_orthonormal {H J : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] [Fintype J] (v : J → H) (hv : Orthonormal ℂ v) :
    ‖∑ j, v j‖ = Real.sqrt (Fintype.card J) := by
…
```
theorem OAI.KadisonSimilarity.tensorWord_mem_submodule line 113
Source documentation
Elementary words linearly span the algebraic tensor power.
```
theorem tensorWord_mem_submodule : ∀ n : ℕ, ∀ S : Submodule ℂ (TensorWord E n),
    (∀ x : Fin n → E, tensorWord x ∈ S) → ∀ z, z ∈ S := by
…
```
Mentions: OAI.KadisonSimilarity.TensorWord, OAI.KadisonSimilarity.tensorWord

theorem OAI.KadisonSimilarity.completedTensorWord_mem_closed_submodule line 140

Source documentation

Elementary words are total after Hilbert completion.

theorem completedTensorWord_mem_closed_submodule {n : ℕ}
    (S : Submodule ℂ (CompletedTensorWord E n))
    (hclosed : IsClosed (S : Set (CompletedTensorWord E n)))
    (hword : ∀ x : Fin n → E, completedTensorWord x ∈ S)
    (z : CompletedTensorWord E n) : z ∈ S := by
…

Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.completedTensorWord

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_completedTensorWords line 153

Source documentation

Continuous operators are determined by their values on elementary words.

theorem continuousLinearMap_ext_completedTensorWords {F : Type*}
    [NormedAddCommGroup F] [NormedSpace ℂ F] {n : ℕ}
    (f g : CompletedTensorWord E n →L[ℂ] F)
    (hword : ∀ x : Fin n → E, f (completedTensorWord x) = g (completedTensorWord x)) : f = g := by
…

Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.completedTensorWord

theorem OAI.KadisonSimilarity.tensorOperator_eq_zero_of_word_coefficients line 168
Source documentation
Vanishing simple-tensor coefficients force a completed tensor operator to be zero. Both input and output totality are proved above.
```
theorem tensorOperator_eq_zero_of_word_coefficients {k l : ℕ}
    (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
    (hword : ∀ (x : Fin k → E) (y : Fin l → E),
      inner ℂ (completedTensorWord y) (Y (completedTensorWord x)) = 0) : Y = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.completedTensorWord