OAI/Analysis/OperatorAlgebra/LpTensorFunctoriality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Contractive tensor maps into the canonical L² operator algebra. The operator structures are fixed before substituting concrete representations.

  1. lemma OAI.WeakPureInfiniteness.lp_norm_minimalSum_map_le line 15