OAI/Probability/ParisiFinite/PacketLabel.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Packet Label.

  1. abbrev OAI.SeedInitialization.PacketLabel line 39
  2. structure OAI.SeedInitialization.CausalStage line 43
  3. def OAI.SeedInitialization.CausalStage.visible line 64
  4. def OAI.SeedInitialization.CausalStage.projections line 67
  5. theorem OAI.SeedInitialization.CausalStage.projections_nonzero line 71
  6. theorem OAI.SeedInitialization.CausalStage.projections_Z line 76
  7. theorem OAI.SeedInitialization.CausalStage.projections_Y line 81
  8. def OAI.SeedInitialization.CausalStage.record line 88
  9. def OAI.SeedInitialization.CausalStage.cost line 121
  10. theorem OAI.SeedInitialization.CausalStage.exists_mixer line 167
  11. def OAI.SeedInitialization.CausalStage.initialCoefficient line 210
  12. theorem OAI.SeedInitialization.CausalStage.initialCenter_coefficient line 213
  13. def OAI.SeedInitialization.CausalStage.initial line 220
  14. def OAI.PointedTree.PacketStage.echoReference line 273
  15. theorem OAI.PointedTree.PacketStage.halfEchoCenter_sub_reference line 277
  16. theorem OAI.PointedTree.PacketStage.halfEchoCenter_close line 301
  17. def OAI.SeedInitialization.CausalStage.echoAngles line 327
  18. def OAI.SeedInitialization.CausalStage.echoCoefficient line 329
  19. def OAI.SeedInitialization.CausalStage.echoCoefficients line 332
  20. def OAI.SeedInitialization.CausalStage.echoTrace line 335
  21. def OAI.SeedInitialization.CausalStage.echoVisible line 338
  22. theorem OAI.SeedInitialization.CausalStage.signed_echo line 341
  23. theorem OAI.SeedInitialization.CausalStage.echo_combination line 346
  24. theorem OAI.SeedInitialization.CausalStage.echo_seed_combination line 355
  25. theorem OAI.SeedInitialization.CausalStage.echo_centerClose line 364
  26. theorem OAI.SeedInitialization.CausalStage.echo_lowClose line 377
  27. def OAI.SeedInitialization.CausalStage.restoredSpin line 409
  28. theorem OAI.SeedInitialization.CausalStage.exists_echo line 430
  29. theorem OAI.SeedInitialization.CausalStage.value_limit line 516
  30. theorem OAI.SeedInitialization.CausalStage.exists_word_close line 527
  31. structure OAI.SeedInitialization.ControlSignature line 546
  32. def OAI.SeedInitialization.ControlSignature.initial line 552
  33. def OAI.SeedInitialization.ControlSignature.mixer line 554
  34. def OAI.SeedInitialization.ControlSignature.cost line 555
  35. def OAI.SeedInitialization.ControlSignature.echo line 556
  36. def OAI.SeedInitialization.ControlSignature.Causal line 559
  37. def OAI.SeedInitialization.ControlSignature.centerTail line 562
  38. def OAI.SeedInitialization.ControlSignature.center line 566
  39. def OAI.SeedInitialization.ControlSignature.visibility line 569
  40. def OAI.SeedInitialization.ControlSignature.Visible line 572
  41. theorem OAI.SeedInitialization.ControlSignature.centerTail_step line 574
  42. theorem OAI.SeedInitialization.ControlSignature.center_step line 588
  43. theorem OAI.SeedInitialization.ControlSignature.causal_succ line 596
  44. theorem OAI.SeedInitialization.ControlSignature.causal_mixer line 599
  45. theorem OAI.SeedInitialization.ControlSignature.causal_cost line 603
  46. theorem OAI.SeedInitialization.ControlSignature.causal_echo line 607
  47. theorem OAI.SeedInitialization.ControlSignature.visibility_step line 615