SpatialTensorFaithful.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Algebraic faithfulness of the spatial product of two faithful representations. Finite coefficient separation uses ordinary linear duals; no simplicity or nuclearity hypothesis occurs.

theorem OAI.WeakPureInfiniteness.spatial_sum_coefficients_zero line 17
def OAI.WeakPureInfiniteness.spatialOperatorBilinear line 39
def OAI.WeakPureInfiniteness.spatialOperatorTensor line 54
theorem OAI.WeakPureInfiniteness.spatialOperatorTensor_injective line 57
theorem OAI.WeakPureInfiniteness.operator_tensor_sum_eq_zero_of_norm_le line 79
Source documentation
A norm-zero spatial finite sum vanishes as an algebraic tensor of operators. Stating this over the Hilbert spaces keeps all operator instances fixed before applying it to bundled representations.
```
theorem operator_tensor_sum_eq_zero_of_norm_le {I : Type*} [Fintype I]
    (a : I → H →L[ℂ] H) (b : I → K →L[ℂ] K)
    (hn : ‖∑ i, TensorProduct.mapL (a i) (b i)‖ ≤ 0) :
    (∑ i, a i ⊗ₜ[ℂ] b i) = 0 := by
…
```