OAI/Probability/ThorpRouting/SparseSaving/InputTree.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

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