OAI/Probability/ThorpRouting/Tail/ParallelFreshPre.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Tail.Thorp.mem_centralBlock line 10
  2. lemma OAI.ThorpNine.Tail.Thorp.centralBlock_card line 22
  3. lemma OAI.ThorpNine.Tail.Thorp.centralBlock_disjoint line 29
  4. lemma OAI.ThorpNine.Tail.Thorp.centralBlock_zero line 38
  5. lemma OAI.ThorpNine.Tail.Thorp.centralBlock_step line 44
  6. lemma OAI.ThorpNine.Tail.Thorp.block_inter_step line 50
  7. lemma OAI.ThorpNine.Tail.Thorp.sparseMass_central_zero line 66
  8. lemma OAI.ThorpNine.Tail.Thorp.sparseMass_central_step line 72
  9. lemma OAI.ThorpNine.Tail.Thorp.inverseButterfly_coordinates_step line 92
  10. lemma OAI.ThorpNine.Tail.Thorp.inverseButterflyMarks_child line 103
  11. lemma OAI.ThorpNine.Tail.Thorp.inverseButterflyMarks_card line 143
  12. lemma OAI.ThorpNine.Tail.Thorp.benes_input_coordinates line 148
  13. lemma OAI.ThorpNine.Tail.Thorp.cutoffMass_central line 154
  14. theorem OAI.ThorpNine.Tail.Thorp.palindrome_low_mgf line 184
  15. def OAI.ThorpNine.Tail.Thorp.parallelFreshPre line 213
  16. def OAI.ThorpNine.Tail.Thorp.parallelFreshPost line 220
  17. def OAI.ThorpNine.Tail.Thorp.parallelAssembled line 224
  18. lemma OAI.ThorpNine.Tail.Thorp.parallel_exposed_perm line 228
  19. theorem OAI.ThorpNine.Tail.Thorp.parallel_partially_exposed_log_mgf line 242
  20. lemma OAI.ThorpNine.Tail.Thorp.orbitSet_inverse line 257
  21. lemma OAI.ThorpNine.Tail.Thorp.selectedCycle_inverse line 261
  22. lemma OAI.ThorpNine.Tail.Thorp.orbitSet_conjugate line 274
  23. def OAI.ThorpNine.Tail.Thorp.conjugateCycle line 287
  24. lemma OAI.ThorpNine.Tail.Thorp.conjugateCycle_injective line 294
  25. lemma OAI.ThorpNine.Tail.Thorp.selectedCycle_conjugate line 300
  26. lemma OAI.ThorpNine.Tail.Thorp.alternatingCycles_le_projection line 322
  27. lemma OAI.ThorpNine.Tail.Thorp.projectionCycles_forward line 331
  28. def OAI.ThorpNine.Tail.Thorp.cycleCoefficient line 353
  29. lemma OAI.ThorpNine.Tail.Thorp.cycleCoefficient_nonneg line 356
  30. lemma OAI.ThorpNine.Tail.Thorp.projectionSide_card_le line 362
  31. theorem OAI.ThorpNine.Tail.Thorp.node_partial_mgf line 369
  32. def OAI.ThorpNine.Tail.Thorp.highStepEquiv line 413
  33. lemma OAI.ThorpNine.Tail.Thorp.assembleBits_step line 430
  34. def OAI.ThorpNine.Tail.Thorp.palindromeLevelCost line 443
  35. lemma OAI.ThorpNine.Tail.Thorp.palindromeLevelCost_step line 456
  36. lemma OAI.ThorpNine.Tail.Thorp.palindromeLevelCost_gt line 471
  37. theorem OAI.ThorpNine.Tail.Thorp.palindrome_level_partial_mgf line 480
  38. def OAI.ThorpNine.Tail.Thorp.switchHeight line 557
  39. lemma OAI.ThorpNine.Tail.Thorp.switchHeight_le line 562
  40. def OAI.ThorpNine.Tail.Thorp.AgreeThrough line 570
  41. def OAI.ThorpNine.Tail.Thorp.LayerAdapted line 573
  42. lemma OAI.ThorpNine.Tail.Thorp.agreeThrough_mono line 576
  43. lemma OAI.ThorpNine.Tail.Thorp.layerAdapted_mono line 580
  44. lemma OAI.ThorpNine.Tail.Thorp.layerAdapted_comp line 584
  45. lemma OAI.ThorpNine.Tail.Thorp.layerAdapted_sum line 588
  46. lemma OAI.ThorpNine.Tail.Thorp.assembleBits_agree line 595
  47. lemma OAI.ThorpNine.Tail.Thorp.palindromeLevelCost_adapted line 608
  48. lemma OAI.ThorpNine.Tail.Thorp.adapted_mul_mean_le line 639
  49. theorem OAI.ThorpNine.Tail.Thorp.cycleCoefficient_decay line 658
  50. lemma OAI.ThorpNine.Tail.Thorp.cycleCutoff_pos line 724
  51. lemma OAI.ThorpNine.Tail.Thorp.pow_sum_le_mean_powers line 731
  52. def OAI.ThorpNine.Tail.Thorp.palindromeSlabCost line 743
  53. lemma OAI.ThorpNine.Tail.Thorp.palindromeSlabCost_adapted line 747
  54. theorem OAI.ThorpNine.Tail.Thorp.palindrome_slab_partial_mgf line 754
  55. lemma OAI.ThorpNine.Tail.Thorp.palindromeSlabCost_gt line 800
  56. lemma OAI.ThorpNine.Tail.Thorp.palindrome_slab_adapted_mul_le line 806
  57. def OAI.ThorpNine.Tail.Thorp.familyEnd line 817
  58. lemma OAI.ThorpNine.Tail.Thorp.familyEnd_two line 819
  59. lemma OAI.ThorpNine.Tail.Thorp.familyEnd_ge line 824
  60. def OAI.ThorpNine.Tail.Thorp.palindromeFamilyCost line 832
  61. lemma OAI.ThorpNine.Tail.Thorp.palindromeFamilyCost_adapted line 836