OAI/Analysis/ModularTheory/StandardTensorBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite tracial core estimates imply the original standard-form tensor bound. Only the supplied nuclear algebra and its quotient are used.

  1. def OAI.WeakPureInfiniteness.modularLpOppositeRepresentation line 18
  2. lemma OAI.WeakPureInfiniteness.modularLpOppositeRepresentation_injective line 24
  3. lemma OAI.WeakPureInfiniteness.modularLp_minimal_sum_norm_le line 31
  4. lemma OAI.WeakPureInfiniteness.nuclear_quotient_modular_coefficients_bound line 44
  5. theorem OAI.WeakPureInfiniteness.nuclear_quotient_standard_tensor_sum_bound line 60