OAI/Analysis/OperatorAlgebra/HilbertTensorExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-sum bounds and minimal tensor completion, with the Hilbert operator structure fixed before a concrete representation is substituted.

  1. lemma OAI.WeakPureInfiniteness.minimalSum_map_norm_le line 12
  2. lemma OAI.WeakPureInfiniteness.hilbert_tensor_algebraic_bound line 26
  3. def OAI.WeakPureInfiniteness.hilbertMinimalTensorExtend line 34
  4. lemma OAI.WeakPureInfiniteness.hilbertMinimalTensorExtend_elementary line 38