OAI/Probability/ParisiFinite/Shape.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Shape.

  1. structure OAI.SeedInitialization.CausalStage.Shape line 43
  2. theorem OAI.SeedInitialization.CausalStage.visibility_shape line 49
  3. theorem OAI.SeedInitialization.CausalStage.visible_shape line 57
  4. theorem OAI.SeedInitialization.CausalStage.record_formal line 63
  5. theorem OAI.SeedInitialization.CausalStage.record_combination line 70
  6. theorem OAI.SeedInitialization.CausalStage.shape_record line 77
  7. theorem OAI.SeedInitialization.CausalStage.shape_initial line 86
  8. theorem OAI.SeedInitialization.CausalStage.shape_cost line 96
  9. theorem OAI.SeedInitialization.CausalStage.record_echo_combination line 105
  10. theorem OAI.SeedInitialization.CausalStage.echo_center_shape line 114
  11. theorem OAI.SeedInitialization.CausalStage.echo_visible_shape line 122
  12. theorem OAI.SeedInitialization.CausalStage.exists_shaped_mixer line 138
  13. theorem OAI.SeedInitialization.CausalStage.exists_shaped_echo line 151
  14. def OAI.SeedInitialization.IndexedControl.depth line 180
  15. def OAI.SeedInitialization.IndexedControl.History line 184
  16. instance OAI.SeedInitialization.IndexedControl.historyFintype line 188
  17. def OAI.SeedInitialization.IndexedControl.signature line 192
  18. theorem OAI.SeedInitialization.IndexedControl.depth_eq line 198
  19. theorem OAI.SeedInitialization.IndexedControl.signature_causal line 203
  20. theorem OAI.SeedInitialization.IndexedControl.signature_word line 213
  21. def OAI.SeedInitialization.IndexedControl.nonzero line 232
  22. def OAI.SeedInitialization.IndexedControl.Admissible line 236
  23. theorem OAI.SeedInitialization.IndexedControl.Admissible.visible line 240
  24. theorem OAI.SeedInitialization.IndexedControl.compile line 248
  25. theorem OAI.SeedInitialization.IndexedControl.exists_word_close line 260
  26. theorem OAI.SeedInitialization.ControlSignature.center_echo line 281
  27. theorem OAI.SeedInitialization.ControlSignature.visibility_stable line 287
  28. theorem OAI.SeedInitialization.IndexedControl.echoCoefficient_half line 301
  29. theorem OAI.SeedInitialization.IndexedControl.echoCoefficient_analytic line 306
  30. theorem OAI.SeedInitialization.IndexedControl.signature_insertion_regular line 315
  31. theorem OAI.SeedInitialization.IndexedControl.center_regular line 325
  32. theorem OAI.SeedInitialization.IndexedControl.visibility_analytic line 344
  33. theorem OAI.SeedInitialization.IndexedControl.center_zero line 351
  34. def OAI.SeedInitialization.IndexedControl.sign line 363
  35. theorem OAI.SeedInitialization.IndexedControl.sign_ne_zero line 365
  36. theorem OAI.SeedInitialization.IndexedControl.visibility_zero line 369
  37. theorem OAI.SeedInitialization.IndexedControl.visibility_zero_ne line 383
  38. def OAI.SeedInitialization.IndexedControl.stages line 404
  39. theorem OAI.SeedInitialization.IndexedControl.mem_stages_self line 408
  40. theorem OAI.SeedInitialization.IndexedControl.admissible_of_stages line 411
  41. theorem OAI.SeedInitialization.IndexedControl.exists_admissible line 425
  42. theorem OAI.SeedInitialization.IndexedControl.exists_ordinary_approx line 462
  43. theorem OAI.SeededTree.circuit_suffix_congr line 486
  44. theorem OAI.SeededTree.value_congr_circuit line 502
  45. def OAI.SeededTree.cancelInitialization line 506
  46. theorem OAI.SeededTree.cancelInitialization_zero line 509
  47. theorem OAI.SeededTree.value_cancelInitialization_zero line 522
  48. def OAI.SeededTree.constantGate line 528
  49. theorem OAI.SeededTree.constantGate_eval line 533
  50. theorem OAI.SeededTree.constantGate_regular line 535
  51. def OAI.SeededTree.initializationCurve line 541
  52. theorem OAI.SeededTree.initializationCurve_eval line 545
  53. theorem OAI.SeededTree.initializationCurve_regular line 555
  54. theorem OAI.SeededTree.exists_small_initialization line 573
  55. def OAI.SeedInitialization.IndexedControl.promote line 596
  56. def OAI.SeedInitialization.IndexedControl.extendedAngles line 601
  57. def OAI.SeedInitialization.IndexedControl.extendedWord line 603
  58. theorem OAI.SeedInitialization.IndexedControl.promote_eval line 606
  59. theorem OAI.SeedInitialization.IndexedControl.promote_word_eval line 610
  60. theorem OAI.SeedInitialization.IndexedControl.extended_initialized_eval line 615
  61. theorem OAI.SeedInitialization.IndexedControl.seed_removal line 629