OAI/Probability/ThorpRouting/Tail/InputTree.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Tail.Thorp.centralDistance_exceptional line 10
  2. inductive OAI.ThorpNine.Tail.Thorp.InputTree line 24
  3. def OAI.ThorpNine.Tail.Thorp.InputTree.perm line 28
  4. def OAI.ThorpNine.Tail.Thorp.InputTree.levelCost line 32
  5. lemma OAI.ThorpNine.Tail.Thorp.InputTree.levelCost_node line 46
  6. lemma OAI.ThorpNine.Tail.Thorp.InputTree.levelCost_gt line 61
  7. lemma OAI.ThorpNine.Tail.Thorp.InputTree.levelCost_adapted line 69
  8. theorem OAI.ThorpNine.Tail.Thorp.InputTree.level_partial_mgf line 100
  9. def OAI.ThorpNine.Tail.Thorp.InputTree.slabCost line 176
  10. lemma OAI.ThorpNine.Tail.Thorp.InputTree.slabCost_adapted line 180
  11. theorem OAI.ThorpNine.Tail.Thorp.InputTree.slab_partial_mgf line 187
  12. def OAI.ThorpNine.Tail.Thorp.boundaryTree line 233
  13. def OAI.ThorpNine.Tail.Thorp.boundaryOutput line 240
  14. lemma OAI.ThorpNine.Tail.Thorp.boundaryOutput_adapted line 246
  15. def OAI.ThorpNine.Tail.Thorp.modifiedBoundary line 261
  16. lemma OAI.ThorpNine.Tail.Thorp.modifiedBoundary_adapted line 265
  17. lemma OAI.ThorpNine.Tail.Thorp.permDistance_boundaryTree line 272
  18. lemma OAI.ThorpNine.Tail.Thorp.boundaryTree_levelCost_perturb line 284
  19. lemma OAI.ThorpNine.Tail.Thorp.boundaryTree_slabCost_perturb line 322
  20. lemma OAI.ThorpNine.Tail.Thorp.modifiedBoundary_distance_le line 332
  21. lemma OAI.ThorpNine.Tail.Thorp.InputTree.slabCost_gt line 340
  22. lemma OAI.ThorpNine.Tail.Thorp.InputTree.random_slab_adapted_mul_le line 347
  23. lemma OAI.ThorpNine.Tail.Thorp.InputTree.slab_mgf line 364
  24. def OAI.ThorpNine.Tail.Thorp.InputTree.familyCost line 374
  25. lemma OAI.ThorpNine.Tail.Thorp.InputTree.random_slabCost_adapted line 379
  26. lemma OAI.ThorpNine.Tail.Thorp.InputTree.familyCost_adapted line 388
  27. theorem OAI.ThorpNine.Tail.Thorp.InputTree.family_mgf_first line 396
  28. lemma OAI.ThorpNine.Tail.Thorp.InputTree.family_mgf_first_decay line 446
  29. def OAI.ThorpNine.Tail.Thorp.modifiedInputTree line 462
  30. lemma OAI.ThorpNine.Tail.Thorp.modifiedInputTree_adapted line 466
  31. lemma OAI.ThorpNine.Tail.Thorp.modified_slab_mgf line 473
  32. lemma OAI.ThorpNine.Tail.Thorp.modified_family_mgf line 499
  33. theorem OAI.ThorpNine.Tail.Thorp.modified_high_mgf line 510
  34. def OAI.ThorpNine.Tail.Thorp.InputTree.lowCost line 539
  35. lemma OAI.ThorpNine.Tail.Thorp.InputTree.lowCost_slab line 543
  36. lemma OAI.ThorpNine.Tail.Thorp.InputTree.cost_family line 550
  37. lemma OAI.ThorpNine.Tail.Thorp.InputTree.lowCost_ge line 564
  38. lemma OAI.ThorpNine.Tail.Thorp.boundaryTree_levelCost_low line 573
  39. lemma OAI.ThorpNine.Tail.Thorp.boundaryTree_lowCost_zero line 582
  40. theorem OAI.ThorpNine.Tail.Thorp.modified_cost_mgf line 590
  41. def OAI.ThorpNine.Tail.Thorp.exceptionChild line 611
  42. lemma OAI.ThorpNine.Tail.Thorp.mem_exceptionChild line 614
  43. lemma OAI.ThorpNine.Tail.Thorp.exceptionChild_card_add line 619
  44. def OAI.ThorpNine.Tail.Thorp.seedSplitEquiv line 629
  45. def OAI.ThorpNine.Tail.Thorp.seedSandwichShuffle line 641
  46. abbrev OAI.ThorpNine.Tail.Thorp.ModifiedCoins line 648
  47. def OAI.ThorpNine.Tail.Thorp.modifiedStepEquiv line 650
  48. def OAI.ThorpNine.Tail.Thorp.modifiedPerm line 655
  49. def OAI.ThorpNine.Tail.Thorp.modifiedCost line 660
  50. lemma OAI.ThorpNine.Tail.Thorp.modifiedBoundary_cons line 664
  51. lemma OAI.ThorpNine.Tail.Thorp.modifiedInputTree_node line 672
  52. lemma OAI.ThorpNine.Tail.Thorp.modifiedPerm_step line 688
  53. lemma OAI.ThorpNine.Tail.Thorp.modifiedPerm_coordinates line 702
  54. lemma OAI.ThorpNine.Tail.Thorp.InputTree.lowCost_node line 712
  55. def OAI.ThorpNine.Tail.Thorp.modifiedAssignmentCost line 741
  56. lemma OAI.ThorpNine.Tail.Thorp.modifiedCost_step line 749
  57. lemma OAI.ThorpNine.Tail.Thorp.PairRouting.childEmbedding_surjective line 771
  58. lemma OAI.ThorpNine.Tail.Thorp.PairRouting.uniformPerm_tuple_upper line 782
  59. def OAI.ThorpNine.Tail.Thorp.centralFactor line 808
  60. lemma OAI.ThorpNine.Tail.Thorp.centralFactor_nonneg line 811
  61. lemma OAI.ThorpNine.Tail.Thorp.centralFactor_step line 814
  62. lemma OAI.ThorpNine.Tail.Thorp.modifiedPerm_zero line 825
  63. lemma OAI.ThorpNine.Tail.Thorp.modifiedCost_zero line 834
  64. lemma OAI.ThorpNine.Tail.Thorp.centralFactor_zero line 839
  65. lemma OAI.ThorpNine.Tail.Thorp.modified_probability_zero_le line 857