OAI/Probability/ThorpRouting/Harmonic/CutoffMass.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Harmonic.Thorp.cutoffMass line 10
  2. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLowCost_eq line 22
  3. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLowCost_le_cutoff line 32
  4. def OAI.ThorpNine.Harmonic.Thorp.centralBlock line 46
  5. lemma OAI.ThorpNine.Harmonic.Thorp.mem_centralBlock line 49
  6. lemma OAI.ThorpNine.Harmonic.Thorp.centralBlock_card line 61
  7. lemma OAI.ThorpNine.Harmonic.Thorp.centralBlock_disjoint line 68
  8. lemma OAI.ThorpNine.Harmonic.Thorp.centralBlock_zero line 77
  9. lemma OAI.ThorpNine.Harmonic.Thorp.centralBlock_step line 83
  10. lemma OAI.ThorpNine.Harmonic.Thorp.block_inter_step line 89
  11. lemma OAI.ThorpNine.Harmonic.Thorp.sparseMass_central_zero line 105
  12. lemma OAI.ThorpNine.Harmonic.Thorp.sparseMass_central_step line 111
  13. lemma OAI.ThorpNine.Harmonic.Thorp.inverseButterfly_coordinates_step line 131
  14. lemma OAI.ThorpNine.Harmonic.Thorp.inverseButterflyMarks_child line 142
  15. lemma OAI.ThorpNine.Harmonic.Thorp.inverseButterflyMarks_card line 182
  16. lemma OAI.ThorpNine.Harmonic.Thorp.benes_input_coordinates line 187
  17. lemma OAI.ThorpNine.Harmonic.Thorp.cutoffMass_central line 193
  18. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_low_mgf line 223
  19. def OAI.ThorpNine.Harmonic.Thorp.parallelFreshPre line 252
  20. def OAI.ThorpNine.Harmonic.Thorp.parallelFreshPost line 259
  21. def OAI.ThorpNine.Harmonic.Thorp.parallelAssembled line 263
  22. lemma OAI.ThorpNine.Harmonic.Thorp.parallel_exposed_perm line 267
  23. theorem OAI.ThorpNine.Harmonic.Thorp.parallel_partially_exposed_log_mgf line 281
  24. lemma OAI.ThorpNine.Harmonic.Thorp.orbitSet_inverse line 296
  25. lemma OAI.ThorpNine.Harmonic.Thorp.selectedCycle_inverse line 300
  26. lemma OAI.ThorpNine.Harmonic.Thorp.orbitSet_conjugate line 313
  27. def OAI.ThorpNine.Harmonic.Thorp.conjugateCycle line 326
  28. lemma OAI.ThorpNine.Harmonic.Thorp.conjugateCycle_injective line 333
  29. lemma OAI.ThorpNine.Harmonic.Thorp.selectedCycle_conjugate line 339
  30. lemma OAI.ThorpNine.Harmonic.Thorp.alternatingCycles_le_projection line 361
  31. lemma OAI.ThorpNine.Harmonic.Thorp.projectionCycles_forward line 370
  32. def OAI.ThorpNine.Harmonic.Thorp.cycleCoefficient line 392
  33. lemma OAI.ThorpNine.Harmonic.Thorp.cycleCoefficient_nonneg line 395
  34. lemma OAI.ThorpNine.Harmonic.Thorp.projectionSide_card_le line 401
  35. theorem OAI.ThorpNine.Harmonic.Thorp.node_partial_mgf line 408
  36. def OAI.ThorpNine.Harmonic.Thorp.highStepEquiv line 452
  37. lemma OAI.ThorpNine.Harmonic.Thorp.assembleBits_step line 469
  38. def OAI.ThorpNine.Harmonic.Thorp.palindromeLevelCost line 482
  39. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLevelCost_step line 495
  40. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLevelCost_gt line 510
  41. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_level_partial_mgf line 519
  42. def OAI.ThorpNine.Harmonic.Thorp.switchHeight line 596
  43. lemma OAI.ThorpNine.Harmonic.Thorp.switchHeight_le line 601
  44. def OAI.ThorpNine.Harmonic.Thorp.AgreeThrough line 609
  45. def OAI.ThorpNine.Harmonic.Thorp.LayerAdapted line 612
  46. lemma OAI.ThorpNine.Harmonic.Thorp.agreeThrough_mono line 615
  47. lemma OAI.ThorpNine.Harmonic.Thorp.layerAdapted_mono line 619
  48. lemma OAI.ThorpNine.Harmonic.Thorp.layerAdapted_comp line 623
  49. lemma OAI.ThorpNine.Harmonic.Thorp.layerAdapted_sum line 627
  50. lemma OAI.ThorpNine.Harmonic.Thorp.assembleBits_agree line 634
  51. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLevelCost_adapted line 647
  52. lemma OAI.ThorpNine.Harmonic.Thorp.adapted_mul_mean_le line 678
  53. theorem OAI.ThorpNine.Harmonic.Thorp.cycleCoefficient_decay line 697
  54. lemma OAI.ThorpNine.Harmonic.Thorp.cycleCutoff_pos line 763
  55. lemma OAI.ThorpNine.Harmonic.Thorp.pow_sum_le_mean_powers line 770
  56. def OAI.ThorpNine.Harmonic.Thorp.palindromeSlabCost line 782
  57. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeSlabCost_adapted line 786
  58. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_slab_partial_mgf line 793
  59. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeSlabCost_gt line 839
  60. lemma OAI.ThorpNine.Harmonic.Thorp.palindrome_slab_adapted_mul_le line 845
  61. def OAI.ThorpNine.Harmonic.Thorp.familyEnd line 856