OAI/Probability/ParisiFinite/UnitaryUp.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Unitary Up.

  1. lemma OAI.HilbertChain.unitary_up line 37
  2. lemma OAI.HilbertChain.embed_unitary_up line 47
  3. def OAI.HilbertChain.unitaryStage line 53
  4. lemma OAI.HilbertChain.unitaryStage_eq line 58
  5. lemma OAI.HilbertChain.unitaryStage_compat line 77
  6. def OAI.HilbertChain.limitIsometry line 88
  7. lemma OAI.HilbertChain.limitIsometry_embed line 91
  8. lemma OAI.HilbertChain.symm_compat line 97
  9. lemma OAI.HilbertChain.limitIsometry_inverse line 102
  10. def OAI.HilbertChain.limitUnitary line 116
  11. lemma OAI.HilbertChain.limitUnitary_embed line 128
  12. lemma OAI.HilbertChain.limitUnitary_symm_embed line 132
  13. def OAI.PointedTree.ordinaryInfinity line 139
  14. theorem OAI.PointedTree.ordinaryInfinity_embed line 143
  15. theorem OAI.PointedTree.ordinaryInfinity_symm_embed line 147
  16. theorem OAI.PointedTree.gammaEmbedding_comp line 159
  17. theorem OAI.PointedTree.modeEmbed_step line 168
  18. def OAI.PointedTree.topFockMap line 173
  19. theorem OAI.PointedTree.topFockMap_step line 176
  20. def OAI.PointedTree.unfoldStage line 190
  21. theorem OAI.PointedTree.unfoldStage_compat line 193
  22. def OAI.PointedTree.unfoldTree line 198
  23. theorem OAI.PointedTree.unfoldTree_embed_succ line 201
  24. theorem OAI.PointedTree.unfoldTree_vacuum line 206
  25. def OAI.PointedTree.spinSingleAux line 213
  26. def OAI.PointedTree.spinSingle line 222
  27. theorem OAI.PointedTree.spinSingle_apply line 225
  28. lemma OAI.PointedTree.spinMap_single line 228
  29. lemma OAI.PointedTree.coherent_in_unfoldTree_range line 236
  30. lemma OAI.PointedTree.spinSingle_in_unfoldTree_range line 250
  31. theorem OAI.PointedTree.unfoldTree_surjective line 264
  32. def OAI.PointedTree.treeFockEquiv line 275
  33. lemma OAI.PointedTree.treeFockEquiv_apply line 278
  34. theorem OAI.HilbertChain.continuous_ext_above line 289
  35. def OAI.PointedTree.rootInfinity line 303
  36. theorem OAI.PointedTree.rootInfinity_embed line 310
  37. theorem OAI.PointedTree.rootInfinity_unfold line 316
  38. theorem OAI.PointedTree.actual_insertionInfinity line 330
  39. theorem OAI.PointedTree.ordinaryInfinity_cost line 339
  40. theorem OAI.PointedTree.ordinaryInfinity_mixer line 356
  41. def OAI.PointedTree.modeFock line 378
  42. def OAI.PointedTree.ordinaryLocal line 381
  43. theorem OAI.PointedTree.ordinaryLocal_apply line 384
  44. theorem OAI.PointedTree.ordinaryLocal_unfold line 387
  45. theorem OAI.PointedTree.ordinaryLocal_nil line 392
  46. theorem OAI.PointedTree.ordinaryLocal_cost line 402
  47. theorem OAI.PointedTree.ordinaryLocal_mixer line 406
  48. theorem OAI.PointedTree.modeFock_insertion line 410
  49. theorem OAI.PointedTree.insertionInfinity_cost line 420
  50. def OAI.PointedTree.toggledProbe line 428
  51. theorem OAI.PointedTree.ordinaryLocal_toggledProbe line 431
  52. theorem OAI.PointedTree.modeFock_rotated_insertion line 439
  53. def OAI.PointedTree.insertionYInfinity line 451
  54. theorem OAI.PointedTree.modeFock_insertionY line 453
  55. theorem OAI.PointedTree.rotated_insertion_eq line 459
  56. abbrev OAI.PointedTree.ShortPulse line 478
  57. def OAI.PointedTree.probePrefix line 481
  58. def OAI.PointedTree.actualProbeDirection line 485
  59. def OAI.PointedTree.actualProbe line 488
  60. def OAI.PointedTree.probeGain line 493
  61. theorem OAI.PointedTree.norm_actualProbeDirection line 497
  62. theorem OAI.PointedTree.probeGain_apply line 500
  63. theorem OAI.PointedTree.probeGain_zero line 504
  64. theorem OAI.PointedTree.probeGain_succ line 508
  65. theorem OAI.PointedTree.probeGain_product line 516
  66. theorem OAI.PointedTree.actual_hermitian_diagonal line 526
  67. theorem OAI.PointedTree.actual_direction_change_bound line 540
  68. theorem OAI.ForwardControl.identity_error_split line 566
  69. theorem OAI.ForwardControl.conjugation_error_split line 581
  70. theorem OAI.CoherentFock.spinMass_prePhaseZ line 601
  71. theorem OAI.CoherentFock.SpinRadiusLE.prePhaseZ line 606
  72. theorem OAI.CoherentFock.spinMass_preProbePhase line 610
  73. theorem OAI.CoherentFock.SpinRadiusLE.preProbePhase line 621
  74. def OAI.CoherentFock.preCenteredProbe line 627
  75. theorem OAI.CoherentFock.spinCoe_preCenteredProbe line 630
  76. theorem OAI.CoherentFock.spinMass_preCenteredProbe line 635
  77. theorem OAI.CoherentFock.SpinRadiusLE.preCenteredProbe line 649
  78. theorem OAI.CoherentFock.spinCoe_coreCentered line 656
  79. theorem OAI.CoherentFock.spinMass_coreCentered line 668
  80. theorem OAI.CoherentFock.radius_coreCentered line 685
  81. theorem OAI.RootSpin.matrixMass_R_le line 706