OAI/Analysis/OInfinity/TensorNorm.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Tensor-norm nuclearity of O∞

Finite unused-generator corners control the Fock matrix in every C*-completion of the algebraic tensor product. The two Gram summands of the return map give a uniform factor-two norm comparison, and the C*-identity removes that factor. This proves the tensor-norm nuclearity input used by the absorption criterion.

  1. lemma OAI.WeakPureInfiniteness.algebraNorm_le_sub_add line 20
  2. lemma OAI.WeakPureInfiniteness.algebraNorm_le_rev_sub_add line 24
  3. lemma OAI.WeakPureInfiniteness.algebraNorm_le_of_approximation line 28
  4. lemma OAI.WeakPureInfiniteness.map_smul_mul line 37
  5. lemma OAI.WeakPureInfiniteness.map_scaled_sum_mul line 44
  6. lemma OAI.WeakPureInfiniteness.map_star_sandwich line 51
  7. lemma OAI.WeakPureInfiniteness.map_scalar_unit_mul line 56
  8. def OAI.WeakPureInfiniteness.fockTensorCoefficient line 72
  9. def OAI.WeakPureInfiniteness.fockTensorBilinear line 84
  10. def OAI.WeakPureInfiniteness.fockTensorMatrix line 98
  11. lemma OAI.WeakPureInfiniteness.fockTensorMatrix_tmul line 102
  12. def OAI.WeakPureInfiniteness.tensorCommutingBilinear line 106
  13. def OAI.WeakPureInfiniteness.tensorCommutingEval line 121
  14. lemma OAI.WeakPureInfiniteness.tensorCommutingEval_tmul line 124
  15. lemma OAI.WeakPureInfiniteness.commuting_vacuum_compression line 127
  16. def OAI.WeakPureInfiniteness.polynomialTensorSum line 151
  17. lemma OAI.WeakPureInfiniteness.exists_tensorApproximation_polynomialSum line 154
  18. lemma OAI.WeakPureInfiniteness.exists_polynomialTensor_alphabet_bound line 170
  19. lemma OAI.WeakPureInfiniteness.commuting_vacuum_compression_list line 183
  20. lemma OAI.WeakPureInfiniteness.fockTensorMatrix_polynomial_norm_le line 199
  21. lemma OAI.WeakPureInfiniteness.mappedFockCuntz_relations line 217
  22. def OAI.WeakPureInfiniteness.representedFockGram line 224
  23. lemma OAI.WeakPureInfiniteness.representedFockGram_apply line 235
  24. lemma OAI.WeakPureInfiniteness.representedFockGram_norm_le line 247
  25. lemma OAI.WeakPureInfiniteness.representedFockGram_tmul line 264
  26. def OAI.WeakPureInfiniteness.representedFockReturn line 282
  27. lemma OAI.WeakPureInfiniteness.representedFockReturn_norm_le line 289
  28. lemma OAI.WeakPureInfiniteness.representedFockReturn_tmul line 307
  29. lemma OAI.WeakPureInfiniteness.representedFockReturn_approximation line 325
  30. lemma OAI.WeakPureInfiniteness.tensor_norm_bound_of_approximation line 337
  31. def OAI.WeakPureInfiniteness.tensorNormLeft line 379
  32. def OAI.WeakPureInfiniteness.tensorNormRight line 391
  33. lemma OAI.WeakPureInfiniteness.tensorNorm_commute line 403
  34. lemma OAI.WeakPureInfiniteness.tensorNorm_support line 407
  35. lemma OAI.WeakPureInfiniteness.tensorNormRight_injective line 415
  36. lemma OAI.WeakPureInfiniteness.tensorNorm_eval line 428
  37. lemma OAI.WeakPureInfiniteness.tensorNorm_fock_return_bound line 438
  38. lemma OAI.WeakPureInfiniteness.tensorNorm_polynomial_bound line 446
  39. lemma OAI.WeakPureInfiniteness.tensorNorm_uniform_bound line 465
  40. theorem OAI.WeakPureInfiniteness.oInfinity_isNuclear line 476

    Source documentation

    The Fock approximation and unused-generator corners give uniqueness of every C*-norm on the algebraic tensor product with OInfinity.

    theorem oInfinity_isNuclear : Pureness.IsNuclear OInfinity := by
…

    Mentions: OAI.Pureness.IsNuclear, OAI.WeakPureInfiniteness.OInfinity