OAI/Probability/ParisiFinite/MixedMatrixOne.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Mixed Matrix One.

  1. theorem OAI.FiniteTensor.mixedMatrix_one line 44
  2. theorem OAI.FiniteTensor.mixedMatrix_mul line 54
  3. theorem OAI.FiniteTensor.mixedMatrix_star line 64
  4. theorem OAI.FiniteTensor.mixedOperator_one line 69
  5. theorem OAI.FiniteTensor.mixedOperator_mul line 73
  6. theorem OAI.FiniteTensor.mixedOperator_star line 78
  7. theorem OAI.FiniteTensor.mixedOperator_projection line 89
  8. theorem OAI.FiniteTensor.vacuumComplement_projection line 105
  9. theorem OAI.FiniteTensor.excitedSlot_projection line 108
  10. theorem OAI.FiniteTensor.excitedSlot_expectation line 118
  11. theorem OAI.TensorPackets.diagonal_projection line 139
  12. theorem OAI.FiniteTree.rootSlot_projection line 157
  13. def OAI.FiniteTree.numberOperator line 170
  14. theorem OAI.FiniteTree.rootSlot_expectation line 173
  15. theorem OAI.FiniteTree.numberOperator_expectation line 183
  16. theorem OAI.FiniteTree.insertion_number_bound line 192
  17. def OAI.RootTensorCLT.constantProgram line 208
  18. theorem OAI.RootTensorCLT.constant_run line 210
  19. theorem OAI.FiniteTree.tensor_Gram_limit line 228
  20. def OAI.FiniteTree.childState line 246
  21. theorem OAI.FiniteTree.norm_childState line 249
  22. theorem OAI.FiniteTree.child_Gram_bound line 253
  23. theorem OAI.FiniteTree.child_Gram_limit line 273
  24. abbrev OAI.FiniteTree.FullRoot.Tail line 294
  25. abbrev OAI.FiniteTree.FullRoot.Space line 295
  26. def OAI.FiniteTree.FullRoot.vac line 297
  27. def OAI.FiniteTree.FullRoot.tensorState line 300
  28. def OAI.FiniteTree.FullRoot.tensorPulse line 303
  29. theorem OAI.FiniteTree.FullRoot.tensor_step line 307
  30. def OAI.FiniteTree.FullRoot.ordinary line 314
  31. def OAI.FiniteTree.FullRoot.insertion line 317
  32. theorem OAI.FiniteTree.FullRoot.run_packet line 320
  33. theorem OAI.FiniteTree.FullRoot.tensor_Gram_factor line 327
  34. theorem OAI.FiniteTree.FullRoot.tensor_Gram_limit line 336
  35. theorem OAI.FiniteTree.FullRoot.program_Gram_limit line 343
  36. theorem OAI.FiniteTree.FullRoot.insertion_Gram_limit line 358
  37. def OAI.FiniteTree.FullRoot.slot line 375
  38. theorem OAI.FiniteTree.FullRoot.slot_projection line 378
  39. def OAI.FiniteTree.FullRoot.occupation line 382
  40. theorem OAI.FiniteTree.FullRoot.tensor_slot_bound line 384
  41. theorem OAI.FiniteTree.FullRoot.packet_slot_bound line 394
  42. theorem OAI.FiniteTree.FullRoot.insertion_slot_bound line 401
  43. theorem OAI.FiniteTree.FullRoot.insertion_occupation_bound line 409
  44. def OAI.FiniteTree.FullRoot.numberOperator line 428
  45. theorem OAI.FiniteTree.FullRoot.slot_expectation line 430
  46. theorem OAI.FiniteTree.FullRoot.number_expectation line 440
  47. theorem OAI.FiniteTree.FullRoot.pulse_exp line 455
  48. theorem OAI.FiniteTree.FullRoot.pulse_unitary line 462
  49. theorem OAI.FiniteTree.FullRoot.pulse_star line 466
  50. theorem OAI.FiniteTree.FullRoot.ordinary_unitary line 475
  51. theorem OAI.FiniteTree.FullRoot.insertion_eq line 486
  52. theorem OAI.FiniteTree.FullRoot.norm_vac line 492
  53. theorem OAI.FiniteTree.FullRoot.norm_insertion line 496
  54. def OAI.FiniteTree.FullRoot.flip line 503
  55. theorem OAI.FiniteTree.FullRoot.flip_unitary line 506
  56. theorem OAI.FiniteTree.FullRoot.flip_square line 509
  57. theorem OAI.FiniteTree.FullRoot.flip_vac line 513
  58. theorem OAI.FiniteTree.FullRoot.flip_star line 518
  59. theorem OAI.FiniteTree.FullRoot.flip_ordinary line 524
  60. theorem OAI.FiniteTree.FullRoot.insertion_odd line 557
  61. theorem OAI.FiniteTree.FullRoot.insertion_centered line 573
  62. def OAI.FiniteTree.FullRoot.excitation line 591
  63. theorem OAI.FiniteTree.FullRoot.excitation_factor line 595
  64. theorem OAI.FiniteTree.FullRoot.sqrt_ratio_limit line 615
  65. theorem OAI.FiniteTree.FullRoot.excitation_tensor_limit line 630
  66. theorem OAI.FiniteTree.FullRoot.root_shift_insertion_limit line 644
  67. theorem OAI.EdgeProjection.decomposition line 673
  68. theorem OAI.EdgeProjection.remainder_bound line 695
  69. theorem OAI.EdgeProjection.real_decomposition line 701