OAI/Probability/ParisiFinite/BranchNumerator.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Branch Numerator.

  1. def OAI.SKCavity.branchNumerator line 64
  2. lemma OAI.SKCavity.branchNumerator_existing line 67
  3. lemma OAI.SKCavity.branchNumerator_fresh line 94
  4. lemma OAI.SKCavity.branchNumerator_one line 117
  5. def OAI.SKCavity.branchEvent line 134
  6. def OAI.SKCavity.branchBlock line 137
  7. lemma OAI.SKCavity.branchBlock_measurable line 140
  8. lemma OAI.SKCavity.branch_existing_iff line 144
  9. lemma OAI.SKCavity.reps_row_le line 156
  10. lemma OAI.SKCavity.branch_fresh_iff line 168
  11. lemma OAI.SKCavity.GG_branch_existing line 183
  12. lemma OAI.SKCavity.GG_branch_fresh line 199
  13. lemma OAI.SKCavity.branch_one_real line 221
  14. theorem OAI.SKCavity.GG_branch_EPPF line 238
  15. lemma OAI.SKCavity.branchNumerator_ordered line 279
  16. def OAI.SKCavity.branchMarkedMoment line 286
  17. theorem OAI.SKCavity.GG_marked_power_derivative line 295
  18. lemma OAI.SKCavity.branchMarkedMoment_nonneg line 313
  19. lemma OAI.SKCavity.branchMarkedMoment_le_ordered line 320
  20. lemma OAI.SKCavity.overlapDiscount_mem_unit line 328
  21. lemma OAI.SKCavity.ordered_range_iff_index line 342
  22. def OAI.SKCavity.blockMax line 353
  23. lemma OAI.SKCavity.blockMax_index line 356
  24. lemma OAI.SKCavity.le_blockMax line 359
  25. lemma OAI.SKCavity.ordered_rel_range line 366
  26. lemma OAI.SKCavity.ordered_rel_max line 372
  27. lemma OAI.SKCavity.ordered_rel_map_mono line 382
  28. theorem OAI.SKCavity.ordered_eq_of_same_relation line 392
  29. lemma OAI.SKCavity.ordered_partition_disjoint line 437
  30. def OAI.SKCavity.Refines line 454
  31. def OAI.SKCavity.NestedCodes line 456
  32. def OAI.SKCavity.hierarchyEvent line 459
  33. def OAI.SKCavity.hierarchyBlock line 462
  34. lemma OAI.SKCavity.hierarchyBlock_measurable line 465
  35. lemma OAI.SKCavity.nestedCodes_restrict line 471
  36. lemma OAI.SKCavity.hierarchy_restrict line 475
  37. lemma OAI.SKCavity.hierarchy_existing_iff line 479
  38. lemma OAI.SKCavity.parentRep_no_join line 493
  39. lemma OAI.SKCavity.hierarchy_fresh_iff line 512
  40. lemma OAI.SKCavity.GG_hierarchy_existing line 537
  41. lemma OAI.SKCavity.GG_hierarchy_fresh line 554
  42. def OAI.SKCavity.childLabels line 583
  43. lemma OAI.SKCavity.mem_childLabels line 586
  44. lemma OAI.SKCavity.childLabels_nonempty line 590
  45. lemma OAI.SKCavity.childLabels_empty line 595
  46. lemma OAI.SKCavity.childLabels_succ line 602
  47. lemma OAI.SKCavity.exists_parentReps line 624
  48. lemma OAI.SKCavity.ParentReps.card_childLabels line 638
  49. def OAI.SKCavity.edgeFactor line 650
  50. def OAI.SKCavity.leafFactor line 653
  51. lemma OAI.SKCavity.edgeFactor_existing line 656
  52. lemma OAI.SKCavity.edgeFactor_fresh_parent line 671
  53. lemma OAI.SKCavity.edgeFactor_fresh_child line 685
  54. lemma OAI.SKCavity.leafFactor_existing line 711
  55. lemma OAI.SKCavity.leafFactor_fresh line 732