OAI/Probability/ParisiFinite/HierarchyNumerator.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Hierarchy Numerator.

  1. def OAI.SKCavity.hierarchyNumerator line 64
  2. lemma OAI.SKCavity.hierarchyNumerator_existing line 68
  3. lemma OAI.SKCavity.hierarchyNumerator_fresh line 84
  4. lemma OAI.SKCavity.codeLabels_one line 121
  5. lemma OAI.SKCavity.childLabels_one line 126
  6. lemma OAI.SKCavity.edgeFactor_one line 131
  7. lemma OAI.SKCavity.leafFactor_one line 134
  8. lemma OAI.SKCavity.hierarchyNumerator_one line 138
  9. lemma OAI.SKCavity.exists_hierarchy_branch line 141
  10. lemma OAI.SKCavity.hierarchy_one_real line 173
  11. theorem OAI.SKCavity.GG_hierarchy_EPPF line 191
  12. def OAI.SKCavity.splitCode line 236
  13. lemma OAI.SKCavity.splitCode_emb line 239
  14. lemma OAI.SKCavity.pair_left_injective line 245
  15. lemma OAI.SKCavity.codeLabels_split line 248
  16. lemma OAI.SKCavity.prod_codeLabels_split line 264
  17. lemma OAI.SKCavity.labelCount_split line 278
  18. lemma OAI.SKCavity.childLabels_split line 291
  19. lemma OAI.SKCavity.leafFactor_split line 312
  20. lemma OAI.SKCavity.edgeFactor_split line 319
  21. lemma OAI.SKCavity.codeLabels_const line 326
  22. lemma OAI.SKCavity.labelCount_const line 331
  23. lemma OAI.SKCavity.leafFactor_const line 334
  24. lemma OAI.SKCavity.edgeFactor_root line 341
  25. def OAI.SKCavity.PartitionTree line 373
  26. instance OAI.SKCavity.partitionTreeFintype line 377
  27. instance OAI.SKCavity.partitionTreeDecidableEq line 384
  28. def OAI.SKCavity.treeCodes line 386
  29. lemma OAI.SKCavity.treeCodes_root line 390
  30. lemma OAI.SKCavity.treeCodes_succ line 395
  31. lemma OAI.SKCavity.splitCode_refines line 399
  32. lemma OAI.SKCavity.treeCodes_nested line 412
  33. lemma OAI.SKCavity.hierarchyNumerator_tree_zero line 426
  34. lemma OAI.SKCavity.hierarchyNumerator_tree_succ line 430
  35. def OAI.SKCavity.hierarchyMark line 465
  36. def OAI.SKCavity.treeMarkMoment line 469
  37. def OAI.SKCavity.hierarchyCoefficient line 473
  38. lemma OAI.SKCavity.hierarchyCoefficient_zero line 477
  39. lemma OAI.SKCavity.hierarchyCoefficient_succ line 484
  40. lemma OAI.SKCavity.hierarchyMark_zero line 516
  41. lemma OAI.SKCavity.hierarchyMark_contDiffAt_zero line 522
  42. lemma OAI.SKCavity.hierarchyMean_derivative line 535
  43. theorem OAI.SKCavity.hierarchyMark_derivative line 550
  44. def OAI.SKCavity.hierarchyLog line 593
  45. lemma OAI.SKCavity.hierarchyLog_derivative line 597
  46. def OAI.SKCavity.hierarchyMarkedMoment line 627
  47. lemma OAI.SKCavity.GG_hierarchy_coefficient line 632
  48. lemma OAI.SKCavity.overlapDiscount_below line 647
  49. theorem OAI.SKCavity.GG_hierarchy_log_derivative line 657
  50. lemma OAI.SKCavity.splitCode_zero_index line 682
  51. lemma OAI.SKCavity.treeCodes_level_one_relation line 690
  52. theorem OAI.SKCavity.tree_eq_of_same_relations line 698
  53. lemma OAI.SKCavity.tree_hierarchy_disjoint line 715
  54. lemma OAI.SKCavity.hierarchyEvent_measurable line 723