OAI/Probability/ParisiFinite/Tensor.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Tensor.

  1. def OAI.TwoHalfTree.tensor line 45
  2. theorem OAI.TwoHalfTree.tensor_apply line 49
  3. theorem OAI.TwoHalfTree.inner_tensor line 52
  4. def OAI.TwoHalfTree.right line 62
  5. def OAI.TwoHalfTree.appendVacuum line 68
  6. theorem OAI.TwoHalfTree.appendVacuum_apply line 80
  7. def OAI.TwoHalfTree.contract line 83
  8. def OAI.TwoHalfTree.projection line 87
  9. theorem OAI.TwoHalfTree.projection_apply line 91
  10. theorem OAI.TwoHalfTree.inner_contract line 95
  11. theorem OAI.TwoHalfTree.contract_tensor_general line 100
  12. theorem OAI.TwoHalfTree.contract_norm_le line 108
  13. theorem OAI.TwoHalfTree.contract_tensor line 119
  14. theorem OAI.TwoHalfTree.projection_isStarProjection line 126
  15. def OAI.TwoHalfTree.swap line 138
  16. theorem OAI.TwoHalfTree.swap_apply line 141
  17. theorem OAI.TwoHalfTree.swap_involutive line 144
  18. theorem OAI.TwoHalfTree.swap_tensor line 149
  19. theorem OAI.TwoHalfTree.swap_selfadjoint line 153
  20. theorem OAI.TwoHalfTree.centered_cross line 159
  21. theorem OAI.TwoHalfTree.single_side_pairing line 166
  22. theorem OAI.TwoHalfTree.edge_decomposition line 173
  23. def OAI.TwoHalfTree.row line 190
  24. theorem OAI.TwoHalfTree.row_apply line 194
  25. def OAI.TwoHalfTree.rightMapLinear line 196
  26. theorem OAI.TwoHalfTree.rightMap_inner line 208
  27. def OAI.TwoHalfTree.rightMap line 220
  28. theorem OAI.TwoHalfTree.rightMap_tensor line 227
  29. theorem OAI.TwoHalfTree.contract_rightMap line 239
  30. theorem OAI.TwoHalfTree.projection_rightMap line 248
  31. theorem OAI.TwoHalfTree.nonvacuum_rightMap_norm line 254
  32. def OAI.FiniteTensor.splitChildIndex line 271
  33. def OAI.FiniteTensor.splitChild line 274
  34. theorem OAI.FiniteTensor.splitChild_apply line 278
  35. theorem OAI.FiniteTensor.splitChild_power line 281
  36. def OAI.FiniteTensor.deleteChild line 290
  37. theorem OAI.FiniteTensor.deleteChild_power line 294
  38. theorem OAI.FiniteTensor.deleteChild_norm_le line 299
  39. def OAI.TensorPackets.liftMap line 312
  40. theorem OAI.TensorPackets.liftMap_apply line 316
  41. theorem OAI.TensorPackets.liftMap_term line 319
  42. theorem OAI.TensorPackets.liftMap_packet line 326
  43. def OAI.TensorEmbedding.matrixPower line 344
  44. theorem OAI.TensorEmbedding.matrixPower_mul line 348
  45. theorem OAI.TensorEmbedding.matrixPower_adjoint line 358
  46. theorem OAI.TensorEmbedding.matrixPower_one line 364
  47. def OAI.TensorEmbedding.map line 367
  48. theorem OAI.TensorEmbedding.map_comp line 372
  49. theorem OAI.TensorEmbedding.map_id line 377
  50. theorem OAI.TensorEmbedding.map_adjoint line 380
  51. theorem OAI.TensorEmbedding.map_inner line 388
  52. def OAI.TensorEmbedding.isometry line 406
  53. theorem OAI.TensorEmbedding.map_power line 414
  54. theorem OAI.TensorEmbedding.isometry_power line 426
  55. def OAI.TensorPackets.liftIsometry line 442
  56. theorem OAI.TensorPackets.liftIsometry_apply line 453
  57. theorem OAI.TensorPackets.liftIsometry_plus line 457
  58. theorem OAI.TensorPackets.liftIsometry_act line 462
  59. def OAI.TensorPackets.scalarVac line 467
  60. theorem OAI.TensorPackets.liftScalarVac_plus line 475
  61. def OAI.FiniteTree.pad line 487
  62. theorem OAI.FiniteTree.split_pad_zero line 494
  63. theorem OAI.FiniteTree.split_pad_succ line 500
  64. theorem OAI.FiniteTree.pad_vac line 506
  65. theorem OAI.FiniteTree.pad_root line 522
  66. theorem OAI.OperatorIntertwine.power line 543
  67. theorem OAI.OperatorIntertwine.exponential line 554
  68. theorem OAI.OperatorIntertwine.adjoint line 570
  69. theorem OAI.TensorEmbedding.map_operator line 594
  70. theorem OAI.TensorEmbedding.isometry_intertwine line 604
  71. theorem OAI.FiniteTree.pad_control line 625
  72. theorem OAI.FiniteTree.Even.pad_observable line 638
  73. theorem OAI.FiniteTree.Even.pad_exponential line 647
  74. theorem OAI.FiniteTree.pad_ordinary line 660
  75. theorem OAI.FiniteTree.pad_insertion line 687