OAI/Probability/ParisiFinite/Labels.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Labels.

  1. def OAI.BoundedBranch.labels line 31
  2. def OAI.BoundedBranch.links line 35
  3. theorem OAI.BoundedBranch.card_labels line 39
  4. theorem OAI.BoundedBranch.map_snd_links line 51
  5. theorem OAI.BoundedBranch.card_links line 66
  6. def OAI.BoundedBranch.unfoldTree line 71
  7. def OAI.BoundedBranch.Parent.layer line 79
  8. lemma OAI.BoundedBranch.Parent.labels_unfold line 81
  9. lemma OAI.BoundedBranch.Parent.links_unfold line 90
  10. lemma OAI.BoundedBranch.Parent.child_layer_iff line 103
  11. theorem OAI.BoundedBranch.Parent.sum_labels_layer line 123
  12. theorem OAI.BoundedBranch.Parent.sum_labels_roots line 162
  13. lemma OAI.BoundedBranch.Parent.links_eq_map_labels line 196
  14. theorem OAI.BoundedBranch.Parent.sum_links_roots line 218
  15. def OAI.SKQAOA.Locality.ball line 238
  16. lemma OAI.SKQAOA.Locality.ball_mono line 242
  17. lemma OAI.SKQAOA.Locality.subset_ball line 247
  18. lemma OAI.SKQAOA.Locality.ball_succ_start line 250
  19. lemma OAI.SKQAOA.Locality.incident_mem_neighborhood line 256
  20. lemma OAI.SKQAOA.Locality.new_vertex_parent line 262
  21. def OAI.SKQAOA.Locality.rank line 285
  22. lemma OAI.SKQAOA.Locality.rank_le_of_mem line 288
  23. lemma OAI.SKQAOA.Locality.mem_ball_rank line 291
  24. lemma OAI.SKQAOA.Locality.rank_zero_iff line 295
  25. theorem OAI.SKQAOA.Locality.exists_parent line 307
  26. theorem OAI.SKQAOA.Locality.relevant_endpoints_in_ball line 339
  27. lemma OAI.SKQAOA.SiteHistories.ball_subset_used line 359
  28. theorem OAI.SKQAOA.SiteHistories.used_eq_ball line 378
  29. def OAI.SKQAOA.FiniteGraph.pairEdges line 407
  30. lemma OAI.SKQAOA.FiniteGraph.mem_pairEdges line 411
  31. def OAI.SKQAOA.FiniteGraph.edgesOfLinks line 438
  32. lemma OAI.SKQAOA.FiniteGraph.mem_edgesOfLinks line 441
  33. lemma OAI.SKQAOA.FiniteGraph.parentEdge_injective line 448
  34. lemma OAI.SKQAOA.FiniteGraph.edge_unique line 475
  35. lemma OAI.SKQAOA.FiniteGraph.edgesOfLinks_parent line 480
  36. abbrev OAI.BoundedBranch.Forest line 500
  37. def OAI.BoundedBranch.forestSize line 502
  38. def OAI.BoundedBranch.forestLabels line 504
  39. def OAI.BoundedBranch.forestLinks line 507
  40. def OAI.BoundedBranch.forestWeight line 510
  41. lemma OAI.BoundedBranch.card_forestLabels line 513
  42. lemma OAI.BoundedBranch.card_forestLinks line 516
  43. lemma OAI.BoundedBranch.map_snd_forestLinks line 519
  44. lemma OAI.BoundedBranch.forestWeight_eq_pow line 523
  45. lemma OAI.BoundedBranch.forestWeight_nonneg line 527
  46. lemma OAI.BoundedBranch.forestWeight_scale line 531
  47. lemma OAI.BoundedBranch.sum_forestWeight line 535
  48. lemma OAI.BoundedBranch.sum_forestWeight_le_tower line 540
  49. lemma OAI.BoundedBranch.forest_tail_bound line 546
  50. def OAI.SKQAOA.SiteHistories.roots line 574
  51. def OAI.SKQAOA.SiteHistories.reached line 575
  52. def OAI.SKQAOA.SiteHistories.distance line 578
  53. lemma OAI.SKQAOA.SiteHistories.exists_parent_pair line 581
  54. def OAI.SKQAOA.SiteHistories.parentPair line 590
  55. lemma OAI.SKQAOA.SiteHistories.parentPair_spec line 594
  56. def OAI.SKQAOA.SiteHistories.parent line 601
  57. def OAI.SKQAOA.SiteHistories.parentEdge line 604
  58. lemma OAI.SKQAOA.SiteHistories.parent_spec line 607
  59. lemma OAI.SKQAOA.SiteHistories.distance_zero line 613
  60. lemma OAI.SKQAOA.SiteHistories.distance_bound line 618
  61. lemma OAI.SKQAOA.SiteHistories.roots_subset_reached line 623
  62. lemma OAI.SKQAOA.SiteHistories.parentEdge_mem line 626
  63. def OAI.SKQAOA.SiteHistories.forestCode line 641
  64. lemma OAI.SKQAOA.SiteHistories.forestCode_labels line 645
  65. lemma OAI.SKQAOA.SiteHistories.forestCode_links line 652
  66. lemma OAI.SKQAOA.SiteHistories.forestCode_size line 660
  67. def OAI.SKQAOA.SiteHistories.forestVertices line 665
  68. def OAI.SKQAOA.SiteHistories.forestEdges line 668
  69. lemma OAI.SKQAOA.SiteHistories.forestCode_vertices line 671
  70. lemma OAI.SKQAOA.SiteHistories.forestCode_edges line 677
  71. lemma OAI.SKQAOA.SiteHistories.forestCode_edges_subset line 682
  72. lemma OAI.SKQAOA.SiteHistories.forestCode_edges_card line 689