OAI/Analysis/FactorGeneration/CornerIndependence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Extension of actual partial unitaries and ordered words from pH. The empty word maps to p, so word transport retains a final p.

  1. def OAI.Generator.Tracial.PartialUnitary.fromRepresentedCorner line 16
  2. theorem OAI.Generator.Tracial.PartialUnitary.fromRepresentedCorner_support_le line 29
  3. theorem OAI.Generator.Tracial.cornerEmbedding_signedLetter line 33
  4. theorem OAI.Generator.Tracial.cornerEmbedding_patchingWord line 39
  5. theorem OAI.Generator.Tracial.cornerEmbedding_patchingWord_nonempty line 48
  6. theorem OAI.Generator.Tracial.cornerEmbedding_trace line 69
  7. theorem OAI.Generator.Tracial.cornerEmbedding_trace_re line 79
  8. theorem OAI.Generator.Tracial.exists_represented_corner_partial_independence line 105
  9. theorem OAI.Generator.Tracial.cornerCompress_norm_le line 159
  10. theorem OAI.Generator.Tracial.cornerCompress_supported line 166
  11. theorem OAI.Generator.Tracial.cornerEmbedding_ordered_tail line 170
  12. theorem OAI.Generator.Tracial.cornerEmbedding_ordered_moment line 192
  13. theorem OAI.Generator.Tracial.exists_varying_corner_partial_independence line 230
  14. theorem OAI.Generator.Tracial.exists_supported_corner_partial_sequence line 327
  15. theorem OAI.Generator.Tracial.exists_quotient_corner_partial_sequence line 352