OAI/Probability/ThorpRouting/Smoothing/BenesCoins.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThorpNine.Smoothing.Thorp.BenesCoins line 12
  2. def OAI.ThorpNine.Smoothing.Thorp.palindromePerm line 14
  3. def OAI.ThorpNine.Smoothing.Thorp.sandwichShuffle line 17
  4. def OAI.ThorpNine.Smoothing.Thorp.benesStepEquiv line 24
  5. lemma OAI.ThorpNine.Smoothing.Thorp.childLift_mul line 28
  6. lemma OAI.ThorpNine.Smoothing.Thorp.childLift_inv line 33
  7. lemma OAI.ThorpNine.Smoothing.Thorp.pairSwitch_inv line 36
  8. lemma OAI.ThorpNine.Smoothing.Thorp.palindromePerm_step line 38
  9. lemma OAI.ThorpNine.Smoothing.Thorp.headTail_switch line 54
  10. lemma OAI.ThorpNine.Smoothing.Thorp.headTail_child line 57
  11. lemma OAI.ThorpNine.Smoothing.Thorp.palindromePerm_coordinates line 60
  12. def OAI.ThorpNine.Smoothing.Thorp.palindromeCost line 69
  13. lemma OAI.ThorpNine.Smoothing.Thorp.CycleColoring.alternating_cycle_two line 85
  14. lemma OAI.ThorpNine.Smoothing.Thorp.CycleColoring.alternating_cycle_count_double line 103
  15. lemma OAI.ThorpNine.Smoothing.Thorp.CycleColoring.alternating_cycle_count_zero line 112
  16. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.alternatingCycles_double line 124
  17. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.alternatingCycles_zero line 129
  18. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.colors_chosenCoin line 138
  19. def OAI.ThorpNine.Smoothing.Thorp.PairRouting.coloredEmbedding line 144
  20. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.coloredEmbedding_apply line 148
  21. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.switchedEmbedding_eq_colored line 155
  22. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.assignments_match_bound line 164
  23. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.occupied_sum_ge line 184
  24. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.assignment_weight_bound line 190
  25. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.assignment_factor_bound line 211
  26. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.sandwich_weighted_probability_subtype line 224
  27. lemma OAI.ThorpNine.Smoothing.Thorp.PairRouting.color_card_add line 235
  28. def OAI.ThorpNine.Smoothing.Thorp.assignmentCost line 245
  29. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeCost_eq line 253
  30. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeCost_step line 263
  31. def OAI.ThorpNine.Smoothing.Thorp.routingMoment line 273
  32. lemma OAI.ThorpNine.Smoothing.Thorp.routingMoment_nonneg line 279
  33. lemma OAI.ThorpNine.Smoothing.Thorp.palindrome_matches_step line 284
  34. lemma OAI.ThorpNine.Smoothing.Thorp.routingMoment_step line 295
  35. lemma OAI.ThorpNine.Smoothing.Thorp.child_moment_product line 338
  36. lemma OAI.ThorpNine.Smoothing.Thorp.palindrome_probability_step line 370
  37. lemma OAI.ThorpNine.Smoothing.Thorp.child_power_product_bound line 385
  38. lemma OAI.ThorpNine.Smoothing.Thorp.assignment_moment_bound line 414
  39. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_pointwise_moment line 453
  40. lemma OAI.ThorpNine.Smoothing.Thorp.routingMoment_sum line 513
  41. lemma OAI.ThorpNine.Smoothing.Thorp.finite_row_power line 535
  42. def OAI.ThorpNine.Smoothing.Thorp.palindromeRowMoment line 544
  43. lemma OAI.ThorpNine.Smoothing.Thorp.density_normalization line 549
  44. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_row_density_moment line 556
  45. lemma OAI.ThorpNine.Smoothing.Thorp.subset_biUnion_indicator line 577
  46. lemma OAI.ThorpNine.Smoothing.Thorp.cylinder_block_polynomial line 597
  47. def OAI.ThorpNine.Smoothing.Thorp.sparseCoefficient line 637
  48. lemma OAI.ThorpNine.Smoothing.Thorp.sparseCoefficient_nonneg line 640
  49. lemma OAI.ThorpNine.Smoothing.Thorp.sparse_block_pointwise line 645
  50. lemma OAI.ThorpNine.Smoothing.Thorp.geometric_sum_half line 665
  51. lemma OAI.ThorpNine.Smoothing.Thorp.sparse_binomial_bound line 674
  52. lemma OAI.ThorpNine.Smoothing.Thorp.sparse_block_product_bound line 708
  53. def OAI.ThorpNine.Smoothing.Thorp.sparseMass line 730
  54. theorem OAI.ThorpNine.Smoothing.Thorp.sparse_block_mgf line 734
  55. theorem OAI.ThorpNine.Smoothing.Thorp.inverseButterfly_sparse_mgf line 770
  56. def OAI.ThorpNine.Smoothing.Thorp.crowdedMass line 783
  57. lemma OAI.ThorpNine.Smoothing.Thorp.crowdedMass_le line 785
  58. lemma OAI.ThorpNine.Smoothing.Thorp.crowdedMass_add line 789
  59. lemma OAI.ThorpNine.Smoothing.Thorp.alternatingCycles_le_crowded line 793
  60. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeCost_le_crowded line 802
  61. def OAI.ThorpNine.Smoothing.Thorp.palindromeLowCost line 826
  62. def OAI.ThorpNine.Smoothing.Thorp.cutoffMass line 839
  63. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeLowCost_eq line 851
  64. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeLowCost_le_cutoff line 861
  65. def OAI.ThorpNine.Smoothing.Thorp.centralBlock line 875