HilbertTensor.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.completion_map_ext line 26

Source documentation

Uniqueness on the dense original normed space.

theorem completion_map_ext {f g : UniformSpace.Completion E →L[ℂ] F}
    (h : ∀ x : E, f x = g x) : f = g := by
…

theorem OAI.NuclearUltrapower.completed_add line 33
theorem OAI.NuclearUltrapower.completed_smul line 39
theorem OAI.NuclearUltrapower.completed_zero line 45
theorem OAI.NuclearUltrapower.completed_comp line 50
theorem OAI.NuclearUltrapower.completed_one line 56
theorem OAI.NuclearUltrapower.completed_norm line 62
Source documentation
Completion does not change an operator norm.
```
@[simp] theorem completed_norm (f : E →L[ℂ] F) : ‖f.completion‖ = ‖f‖ := by
…
```
abbrev OAI.NuclearUltrapower.TensorHilbert line 74
def OAI.NuclearUltrapower.completedTensorMap line 81
theorem OAI.NuclearUltrapower.completedTensorMap_coe line 84
theorem OAI.NuclearUltrapower.tensorMap_one line 88
theorem OAI.NuclearUltrapower.completedTensorMap_one line 94
theorem OAI.NuclearUltrapower.completedTensorMap_mul line 97
theorem OAI.NuclearUltrapower.completedTensorMap_add_left line 103
theorem OAI.NuclearUltrapower.completedTensorMap_add_right line 107
theorem OAI.NuclearUltrapower.completedTensorMap_smul_left line 111
theorem OAI.NuclearUltrapower.completedTensorMap_smul_right line 115
theorem OAI.NuclearUltrapower.completedTensorMap_zero_left line 119
theorem OAI.NuclearUltrapower.completedTensorMap_zero_right line 122
theorem OAI.NuclearUltrapower.completedTensorMap_norm_le line 126
Source documentation
The elementary tensor bound, including unequal varying dimensions.
```
theorem completedTensorMap_norm_le (U : E →L[ℂ] E) (V : F →L[ℂ] F) :
    ‖completedTensorMap U V‖ ≤ ‖U‖ * ‖V‖ := by
…
```
Mentions: OAI.NuclearUltrapower.completedTensorMap
theorem OAI.NuclearUltrapower.completedTensorMap_star line 134
Source documentation
Adjoint compatibility proved on the dense tensor product, not by assuming it complete.
```
@[simp] theorem completedTensorMap_star (U : E →L[ℂ] E) (V : F →L[ℂ] F) :
    completedTensorMap (star U) (star V) = star (completedTensorMap U V) := by
…
```
Mentions: OAI.NuclearUltrapower.completedTensorMap
def OAI.NuclearUltrapower.tensorLeftHom line 155
Source documentation
The two commuting unital coordinate tensor embeddings.
```
def tensorLeftHom : (E →L[ℂ] E) →⋆ₐ[ℂ] (TensorHilbert E F →L[ℂ] TensorHilbert E F) where
…
```
Mentions: OAI.NuclearUltrapower.TensorHilbert
def OAI.NuclearUltrapower.tensorRightHom line 166
theorem OAI.NuclearUltrapower.tensorLeftRight_mul line 177
theorem OAI.NuclearUltrapower.tensorLeftRight_commute line 182