OAI/Probability/ThorpRouting/Harmonic/SandwichShuffle.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

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