OAI/Analysis/Nuclearity/SpatialEvaluation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Faithful spatial representations of the minimal completion.

  1. def OAI.WeakPureInfiniteness.minimalSpatialEvaluation line 17

    Source documentation

    Evaluation at one of the spatial representations defining the norm.

    def minimalSpatialEvaluation (π : SpatialRepresentation A B) :
    MinimalTensor A B →⋆ₙₐ[ℂ] (π.space →L[ℂ] π.space) where
…

    Mentions: OAI.WeakPureInfiniteness.SpatialRepresentation, OAI.WeakPureInfiniteness.MinimalTensor

  2. theorem OAI.WeakPureInfiniteness.minimalSpatialEvaluation_elementary line 26
  3. theorem OAI.WeakPureInfiniteness.norm_spatialSum_le_faithful line 31
  4. theorem OAI.WeakPureInfiniteness.minimalSpatialEvaluation_norm_sum line 54
  5. theorem OAI.WeakPureInfiniteness.minimalSpatialEvaluation_isometry line 72