OAI/Probability/ThorpRouting/Casimir/InputTree.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Casimir.Thorp.centralSlabCost_perturb line 10
  2. lemma OAI.ThorpNine.Casimir.Thorp.centralDistance_exceptional line 18
  3. inductive OAI.ThorpNine.Casimir.Thorp.InputTree line 32
  4. def OAI.ThorpNine.Casimir.Thorp.InputTree.perm line 36
  5. def OAI.ThorpNine.Casimir.Thorp.InputTree.levelCost line 40
  6. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.levelCost_node line 54
  7. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.levelCost_gt line 69
  8. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.levelCost_adapted line 77
  9. theorem OAI.ThorpNine.Casimir.Thorp.InputTree.level_partial_mgf line 108
  10. def OAI.ThorpNine.Casimir.Thorp.InputTree.slabCost line 184
  11. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.slabCost_adapted line 188
  12. theorem OAI.ThorpNine.Casimir.Thorp.InputTree.slab_partial_mgf line 195
  13. def OAI.ThorpNine.Casimir.Thorp.boundaryTree line 241
  14. def OAI.ThorpNine.Casimir.Thorp.boundaryOutput line 248
  15. lemma OAI.ThorpNine.Casimir.Thorp.boundaryOutput_adapted line 254
  16. def OAI.ThorpNine.Casimir.Thorp.modifiedBoundary line 269
  17. lemma OAI.ThorpNine.Casimir.Thorp.modifiedBoundary_adapted line 273
  18. lemma OAI.ThorpNine.Casimir.Thorp.permDistance_boundaryTree line 280
  19. lemma OAI.ThorpNine.Casimir.Thorp.boundaryTree_levelCost_perturb line 292
  20. lemma OAI.ThorpNine.Casimir.Thorp.boundaryTree_slabCost_perturb line 330
  21. lemma OAI.ThorpNine.Casimir.Thorp.modifiedBoundary_distance_le line 340
  22. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.slabCost_gt line 348
  23. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.random_slab_adapted_mul_le line 355
  24. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.slab_mgf line 372
  25. def OAI.ThorpNine.Casimir.Thorp.InputTree.familyCost line 382
  26. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.random_slabCost_adapted line 387
  27. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.familyCost_adapted line 396
  28. theorem OAI.ThorpNine.Casimir.Thorp.InputTree.family_mgf_first line 404
  29. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.family_mgf_first_decay line 454
  30. def OAI.ThorpNine.Casimir.Thorp.modifiedInputTree line 470
  31. lemma OAI.ThorpNine.Casimir.Thorp.modifiedInputTree_adapted line 474
  32. lemma OAI.ThorpNine.Casimir.Thorp.modified_slab_mgf line 481
  33. lemma OAI.ThorpNine.Casimir.Thorp.modified_family_mgf line 507
  34. theorem OAI.ThorpNine.Casimir.Thorp.modified_high_mgf line 518
  35. def OAI.ThorpNine.Casimir.Thorp.InputTree.lowCost line 547
  36. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.lowCost_slab line 551
  37. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.cost_family line 558
  38. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.lowCost_ge line 572
  39. lemma OAI.ThorpNine.Casimir.Thorp.boundaryTree_levelCost_low line 581
  40. lemma OAI.ThorpNine.Casimir.Thorp.boundaryTree_lowCost_zero line 590
  41. theorem OAI.ThorpNine.Casimir.Thorp.modified_cost_mgf line 598
  42. def OAI.ThorpNine.Casimir.Thorp.exceptionChild line 619
  43. lemma OAI.ThorpNine.Casimir.Thorp.mem_exceptionChild line 622
  44. lemma OAI.ThorpNine.Casimir.Thorp.exceptionChild_card_add line 627
  45. def OAI.ThorpNine.Casimir.Thorp.seedSplitEquiv line 637
  46. def OAI.ThorpNine.Casimir.Thorp.seedSandwichShuffle line 649
  47. abbrev OAI.ThorpNine.Casimir.Thorp.ModifiedCoins line 656
  48. def OAI.ThorpNine.Casimir.Thorp.modifiedStepEquiv line 658
  49. def OAI.ThorpNine.Casimir.Thorp.modifiedPerm line 663
  50. def OAI.ThorpNine.Casimir.Thorp.modifiedCost line 668
  51. lemma OAI.ThorpNine.Casimir.Thorp.modifiedBoundary_cons line 672
  52. lemma OAI.ThorpNine.Casimir.Thorp.modifiedInputTree_node line 680
  53. lemma OAI.ThorpNine.Casimir.Thorp.modifiedPerm_step line 696
  54. lemma OAI.ThorpNine.Casimir.Thorp.modifiedPerm_coordinates line 710
  55. lemma OAI.ThorpNine.Casimir.Thorp.InputTree.lowCost_node line 720
  56. def OAI.ThorpNine.Casimir.Thorp.modifiedAssignmentCost line 749
  57. lemma OAI.ThorpNine.Casimir.Thorp.modifiedCost_step line 757
  58. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.childEmbedding_surjective line 779
  59. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.uniformPerm_tuple_upper line 790
  60. def OAI.ThorpNine.Casimir.Thorp.centralFactor line 816
  61. lemma OAI.ThorpNine.Casimir.Thorp.centralFactor_nonneg line 819
  62. lemma OAI.ThorpNine.Casimir.Thorp.centralFactor_step line 822
  63. lemma OAI.ThorpNine.Casimir.Thorp.modifiedPerm_zero line 833
  64. lemma OAI.ThorpNine.Casimir.Thorp.modifiedCost_zero line 842
  65. lemma OAI.ThorpNine.Casimir.Thorp.centralFactor_zero line 847