OAI/Probability/ParisiFinite/UsedVertices.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Used Vertices.

  1. def OAI.SKQAOA.SiteHistories.usedVertices line 32
  2. lemma OAI.SKQAOA.SiteHistories.fst_mem_usedVertices line 35
  3. lemma OAI.SKQAOA.SiteHistories.snd_mem_usedVertices line 39
  4. lemma OAI.SKQAOA.SiteHistories.card_usedVertices_le line 43
  5. lemma OAI.SKQAOA.SiteHistories.rootFactor_local line 57
  6. lemma OAI.SKQAOA.SiteHistories.cluster_integrand_local line 63
  7. lemma OAI.SKQAOA.SiteHistories.norm_rootFactor_le line 76
  8. lemma OAI.SKQAOA.SiteHistories.norm_factor_sub_one_le line 91
  9. theorem OAI.SKQAOA.SiteHistories.norm_cluster_le_local line 102
  10. def OAI.SKQAOA.SiteHistories.variation line 122
  11. lemma OAI.SKQAOA.SiteHistories.one_le_variation line 124
  12. def OAI.SKQAOA.SiteHistories.activity line 128
  13. def OAI.SKQAOA.SiteHistories.markedBound line 131
  14. lemma OAI.SKQAOA.SiteHistories.activity_nonneg line 134
  15. lemma OAI.SKQAOA.SiteHistories.markedBound_nonneg line 138
  16. theorem OAI.SKQAOA.SiteHistories.norm_cluster_le line 144
  17. def OAI.SKQAOA.SiteHistories.edgeMap line 176
  18. lemma OAI.SKQAOA.SiteHistories.edgeMap_fst line 184
  19. lemma OAI.SKQAOA.SiteHistories.edgeMap_snd line 186
  20. lemma OAI.SKQAOA.SiteHistories.usedVertices_map line 189
  21. theorem OAI.SKQAOA.SiteHistories.graphCoefficient_relabel line 203
  22. def OAI.SKQAOA.SiteHistories.rawGraphCoefficient line 222
  23. lemma OAI.SKQAOA.SiteHistories.graphCoefficient_eq_pow_mul_raw line 230
  24. lemma OAI.SKQAOA.SiteHistories.cluster_eq_inv_sqrt_mul_raw line 244
  25. lemma OAI.SKQAOA.SiteHistories.cluster_eq_scaled line 258
  26. abbrev OAI.SKQAOA.SiteHistories.MarkedGraph line 277
  27. abbrev OAI.SKQAOA.SiteHistories.FullGraph line 278
  28. abbrev OAI.SKQAOA.SiteHistories.SupportSet line 279
  29. def OAI.SKQAOA.SiteHistories.graphMap line 281
  30. lemma OAI.SKQAOA.SiteHistories.graphMap_injective line 284
  31. lemma OAI.SKQAOA.SiteHistories.graphMap_support line 290
  32. lemma OAI.SKQAOA.SiteHistories.edgeMap_surjective_on line 294
  33. lemma OAI.SKQAOA.SiteHistories.graphMap_surjective_on line 308
  34. def OAI.SKQAOA.SiteHistories.embedFullGraph line 336
  35. lemma OAI.SKQAOA.SiteHistories.embedFullGraph_support line 342
  36. lemma OAI.SKQAOA.SiteHistories.embedFullGraph_bijective line 347
  37. def OAI.SKQAOA.SiteHistories.supportGraphEquiv line 362
  38. lemma OAI.SKQAOA.SiteHistories.card_supportSet line 366
  39. theorem OAI.SKQAOA.SiteHistories.sum_full_graphs line 375
  40. def OAI.BoundedBranch.Tree line 396
  41. instance OAI.BoundedBranch.treeFintype line 400
  42. def OAI.BoundedBranch.size line 405
  43. def OAI.BoundedBranch.weight line 409
  44. def OAI.BoundedBranch.partition line 413
  45. theorem OAI.BoundedBranch.partition_zero line 415
  46. theorem OAI.BoundedBranch.weight_nonneg line 419
  47. theorem OAI.BoundedBranch.partition_nonneg line 430
  48. theorem OAI.BoundedBranch.partition_succ line 434
  49. def OAI.BoundedBranch.tower line 444
  50. theorem OAI.BoundedBranch.tower_pos line 448
  51. theorem OAI.BoundedBranch.partition_step_bound line 453
  52. theorem OAI.BoundedBranch.partition_le_tower line 470
  53. theorem OAI.BoundedBranch.weight_eq_pow line 478
  54. theorem OAI.BoundedBranch.weight_scale line 492
  55. def OAI.BoundedBranch.tail line 496
  56. theorem OAI.BoundedBranch.tail_bound line 501
  57. theorem OAI.BoundedBranch.uniform_tail line 522