OAI/Analysis/ModularTheory/CornerTensorBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite tracial estimates pass through the actual GNS corner inclusions and the strongly exhausting two-sided projections.

  1. lemma OAI.WeakPureInfiniteness.modularCoreCompression_product_sum line 20
  2. abbrev OAI.WeakPureInfiniteness.modularCoreCompression_minimal_sum_bound line 40
  3. abbrev OAI.WeakPureInfiniteness.modular_lifted_compressed_sum_proof line 54
  4. theorem OAI.WeakPureInfiniteness.modular_lifted_compressed_sum_bound line 80
  5. lemma OAI.WeakPureInfiniteness.nuclear_quotient_modular_compressed_sum_bound line 89
  6. theorem OAI.WeakPureInfiniteness.nuclear_quotient_modular_finite_sum_bound line 104