OAI/Analysis/CharacterCriterion/Traces.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KirchbergRordam.Traces.State line 39
  2. lemma OAI.KirchbergRordam.Traces.bound line 45
  3. def OAI.KirchbergRordam.Traces.pullback line 47
  4. def OAI.KirchbergRordam.Traces.positive line 55
  5. lemma OAI.KirchbergRordam.Traces.positive_apply line 57
  6. lemma OAI.KirchbergRordam.Traces.conjugation line 58
  7. def OAI.KirchbergRordam.Traces.matrixLinear line 64
  8. lemma OAI.KirchbergRordam.Traces.matrixLinear_apply line 67
  9. lemma OAI.KirchbergRordam.Traces.matrixLinear_bound line 74
  10. def OAI.KirchbergRordam.Traces.matrixState line 82
  11. lemma OAI.KirchbergRordam.Traces.exists_extension line 95
  12. theorem OAI.KirchbergRordam.Traces.exists_inductive_trace line 117
  13. def OAI.KirchbergRordam.Traces.tensorRepresentation line 162
  14. lemma OAI.KirchbergRordam.Traces.tensorRepresentation_tmul line 167
  15. abbrev OAI.KirchbergRordam.Traces.productHilbert line 178
  16. def OAI.KirchbergRordam.Traces.productRep line 179
  17. def OAI.KirchbergRordam.Traces.productVector line 181
  18. lemma OAI.KirchbergRordam.Traces.unitVector_norm line 184
  19. lemma OAI.KirchbergRordam.Traces.productVector_norm line 189
  20. def OAI.KirchbergRordam.Traces.productFunctional line 191
  21. lemma OAI.KirchbergRordam.Traces.productFunctional_apply line 195
  22. lemma OAI.KirchbergRordam.Traces.productFunctional_tmul line 197
  23. lemma OAI.KirchbergRordam.Traces.productFunctional_bound line 208
  24. lemma OAI.KirchbergRordam.Traces.productFunctional_one line 218
  25. lemma OAI.KirchbergRordam.Traces.productFunctional_trace line 226
  26. def OAI.KirchbergRordam.Traces.product line 260
  27. lemma OAI.KirchbergRordam.Traces.product_left line 265
  28. lemma OAI.KirchbergRordam.Traces.product_right line 268
  29. lemma OAI.KirchbergRordam.Traces.State.ext line 274
  30. theorem OAI.KirchbergRordam.Traces.unique_of_halfFlip line 282
  31. def OAI.KirchbergRordam.BalancedDropLimit.stageTrace line 300
  32. theorem OAI.KirchbergRordam.BalancedDropLimit.trace_exists line 303
  33. theorem OAI.KirchbergRordam.BalancedDropLimit.trace_unique line 305
  34. def OAI.KirchbergRordam.BalancedDropLimit.uniqueTrace line 309