OAI/Probability/ThorpRouting/Casimir/SandwichShuffle.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.sandwich_power_bound line 14
  2. def OAI.ThorpNine.Casimir.Thorp.sandwichShuffle line 53
  3. def OAI.ThorpNine.Casimir.Thorp.benesStepEquiv line 60
  4. lemma OAI.ThorpNine.Casimir.Thorp.childLift_mul line 64
  5. lemma OAI.ThorpNine.Casimir.Thorp.childLift_inv line 69
  6. lemma OAI.ThorpNine.Casimir.Thorp.pairSwitch_inv line 72
  7. lemma OAI.ThorpNine.Casimir.Thorp.palindromePerm_step line 74
  8. lemma OAI.ThorpNine.Casimir.Thorp.headTail_switch line 90
  9. lemma OAI.ThorpNine.Casimir.Thorp.headTail_child line 93
  10. lemma OAI.ThorpNine.Casimir.Thorp.palindromePerm_coordinates line 96
  11. def OAI.ThorpNine.Casimir.Thorp.palindromeCost line 105
  12. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.alternating_cycle_two line 121
  13. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.alternating_cycle_count_double line 139
  14. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.alternating_cycle_count_zero line 148
  15. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.alternatingCycles_double line 160
  16. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.alternatingCycles_zero line 165
  17. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.colors_chosenCoin line 174
  18. def OAI.ThorpNine.Casimir.Thorp.PairRouting.coloredEmbedding line 180
  19. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.coloredEmbedding_apply line 184
  20. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.switchedEmbedding_eq_colored line 191
  21. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.assignments_match_bound line 200
  22. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.occupied_sum_ge line 220
  23. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.assignment_weight_bound line 226
  24. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.assignment_factor_bound line 247
  25. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.sandwich_weighted_probability_subtype line 260
  26. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.color_card_add line 271
  27. def OAI.ThorpNine.Casimir.Thorp.assignmentCost line 281
  28. lemma OAI.ThorpNine.Casimir.Thorp.palindromeCost_eq line 289
  29. lemma OAI.ThorpNine.Casimir.Thorp.palindromeCost_step line 299
  30. def OAI.ThorpNine.Casimir.Thorp.routingMoment line 309
  31. lemma OAI.ThorpNine.Casimir.Thorp.routingMoment_nonneg line 315
  32. lemma OAI.ThorpNine.Casimir.Thorp.palindrome_matches_step line 320
  33. lemma OAI.ThorpNine.Casimir.Thorp.routingMoment_step line 331
  34. lemma OAI.ThorpNine.Casimir.Thorp.child_moment_product line 374
  35. lemma OAI.ThorpNine.Casimir.Thorp.palindrome_probability_step line 406
  36. lemma OAI.ThorpNine.Casimir.Thorp.child_power_product_bound line 421
  37. lemma OAI.ThorpNine.Casimir.Thorp.assignment_moment_bound line 450
  38. theorem OAI.ThorpNine.Casimir.Thorp.palindrome_pointwise_moment line 489
  39. lemma OAI.ThorpNine.Casimir.Thorp.routingMoment_sum line 549
  40. lemma OAI.ThorpNine.Casimir.Thorp.finite_row_power line 571
  41. lemma OAI.ThorpNine.Casimir.Thorp.density_normalization line 580
  42. theorem OAI.ThorpNine.Casimir.Thorp.palindrome_row_density_moment line 587
  43. lemma OAI.ThorpNine.Casimir.Thorp.subset_biUnion_indicator line 608
  44. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_block_polynomial line 628
  45. def OAI.ThorpNine.Casimir.Thorp.sparseCoefficient line 668
  46. lemma OAI.ThorpNine.Casimir.Thorp.sparseCoefficient_nonneg line 671
  47. lemma OAI.ThorpNine.Casimir.Thorp.sparse_block_pointwise line 676
  48. lemma OAI.ThorpNine.Casimir.Thorp.geometric_sum_half line 696
  49. lemma OAI.ThorpNine.Casimir.Thorp.sparse_binomial_bound line 705
  50. lemma OAI.ThorpNine.Casimir.Thorp.sparse_block_product_bound line 739
  51. def OAI.ThorpNine.Casimir.Thorp.sparseMass line 761
  52. theorem OAI.ThorpNine.Casimir.Thorp.sparse_block_mgf line 765
  53. theorem OAI.ThorpNine.Casimir.Thorp.inverseButterfly_sparse_mgf line 801
  54. def OAI.ThorpNine.Casimir.Thorp.crowdedMass line 814
  55. lemma OAI.ThorpNine.Casimir.Thorp.crowdedMass_le line 816
  56. lemma OAI.ThorpNine.Casimir.Thorp.crowdedMass_add line 820
  57. lemma OAI.ThorpNine.Casimir.Thorp.alternatingCycles_le_crowded line 824
  58. lemma OAI.ThorpNine.Casimir.Thorp.palindromeCost_le_crowded line 833
  59. def OAI.ThorpNine.Casimir.Thorp.palindromeLowCost line 857