OAI/Probability/ParisiFinite/InsertionApprox.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Insertion Approx.

  1. theorem OAI.PointedTree.PacketStage.insertion_approx line 42
  2. theorem OAI.PointedTree.PacketStage.insertionZ_approx line 52
  3. theorem OAI.PointedTree.PacketStage.insertionY_approx line 58
  4. theorem OAI.PointedTree.PacketStage.huge_transverse_approx line 66
  5. theorem OAI.PointedTree.PacketStage.forwardCenter_approx line 84
  6. def OAI.GramCalculus.combination line 110
  7. theorem OAI.GramCalculus.combination_add line 112
  8. theorem OAI.GramCalculus.combination_neg line 116
  9. theorem OAI.GramCalculus.combination_smul line 120
  10. theorem OAI.GramCalculus.combination_zero line 124
  11. def OAI.GramCalculus.GramConverges line 127
  12. theorem OAI.GramCalculus.GramConverges.combinations line 133
  13. theorem OAI.GramCalculus.GramConverges.phase line 143
  14. theorem OAI.GramCalculus.GramConverges.norm_combination line 152
  15. theorem OAI.GramCalculus.GramConverges.combination_bounded line 159
  16. theorem OAI.GramCalculus.spinPacket_reindex line 167
  17. def OAI.GramCalculus.PacketMatch line 187
  18. theorem OAI.GramCalculus.PacketMatch.vacuum line 197
  19. theorem OAI.GramCalculus.PacketMatch.root line 203
  20. theorem OAI.GramCalculus.PacketMatch.smul line 212
  21. theorem OAI.GramCalculus.PacketMatch.pulse line 222
  22. theorem OAI.GramCalculus.PacketMatch.inner line 253
  23. theorem OAI.GramCalculus.PacketMatch.creation line 267
  24. theorem OAI.GramCalculus.PacketMatch.norm line 295
  25. def OAI.GramCalculus.ApproxMatch line 305
  26. theorem OAI.GramCalculus.PacketMatch.approx line 309
  27. theorem OAI.GramCalculus.ApproxMatch.close line 316
  28. theorem OAI.GramCalculus.ApproxMatch.norm line 324
  29. theorem OAI.GramCalculus.ApproxMatch.norm_bounded line 333
  30. theorem OAI.GramCalculus.ApproxMatch.inner line 339
  31. theorem OAI.GramCalculus.ApproxMatch.creation line 359
  32. inductive OAI.GramCalculus.WeylGate line 389
  33. def OAI.GramCalculus.WeylGate.op line 397
  34. def OAI.GramCalculus.WeylGate.inv line 401
  35. theorem OAI.GramCalculus.WeylGate.op_inv line 405
  36. theorem OAI.GramCalculus.WeylGate.packet_match line 410
  37. theorem OAI.GramCalculus.WeylGate.bounded line 417
  38. def OAI.GramCalculus.WeylWord.op line 430
  39. theorem OAI.GramCalculus.WeylWord.op_nil line 434
  40. theorem OAI.GramCalculus.WeylWord.op_cons line 435
  41. theorem OAI.GramCalculus.WeylWord.op_append line 438
  42. def OAI.GramCalculus.WeylWord.inv line 444
  43. theorem OAI.GramCalculus.WeylWord.op_inv line 446
  44. theorem OAI.GramCalculus.WeylWord.packet_match line 457
  45. theorem OAI.GramCalculus.WeylWord.bounded line 464
  46. theorem OAI.GramCalculus.WeylWord.insertion_match line 473
  47. theorem OAI.CoherentFock.BoundedPacket.pulse_close line 492
  48. def OAI.CoherentFock.PacketUnitaryFamily.LowClose line 507
  49. theorem OAI.CoherentFock.PacketUnitaryFamily.LowClose.refl line 513
  50. theorem OAI.CoherentFock.PacketUnitaryFamily.LowClose.symm line 517
  51. theorem OAI.CoherentFock.PacketUnitaryFamily.LowClose.trans line 521
  52. theorem OAI.CoherentFock.PacketUnitaryFamily.LowClose.comp line 527
  53. theorem OAI.CoherentFock.PacketUnitaryFamily.LowClose.inverse line 538
  54. theorem OAI.CoherentFock.PacketUnitaryFamily.LowClose.insertion line 547
  55. theorem OAI.CoherentFock.PacketUnitaryFamily.pulse_lowClose line 558
  56. theorem OAI.PointedTree.PacketStage.halfEcho_transport_exact line 581
  57. theorem OAI.PointedTree.PacketStage.Transported.halfEcho line 600
  58. theorem OAI.CoherentFock.negativeHalfMixer_sector line 645
  59. theorem OAI.CoherentFock.negative_half_mixer_anticommutes line 653
  60. theorem OAI.CoherentFock.PacketExpansion.negative_half_mixer line 661