OAI/Probability/ThorpRouting/Dense/SingleSlotsEquiv.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.singleSlotsEquiv line 13
  2. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.cycleCount line 27
  3. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.cycleCount_eq_sum line 30
  4. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.hasSum_cycleCount_weight line 35
  5. lemma OAI.ThorpNine.Dense.Thorp.hasSum_finiteMean line 59
  6. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.selected_cycle_mean_le_h line 70
  7. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.reciprocal_values_nonempty line 134
  8. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.h_nonneg line 151
  9. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.h_le_one line 155
  10. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.law_reciprocal_cutoff line 158
  11. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.h_cutoff line 186
  12. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.h_dyadic_bound line 191
  13. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.summable_half_dyadic line 206
  14. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.h_summable line 222
  15. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.allocation_value_summable line 225
  16. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.H_values_bdd line 230
  17. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.allocation_le_H line 238
  18. def OAI.ThorpNine.Dense.Thorp.unitCardEquiv line 247
  19. def OAI.ThorpNine.Dense.Thorp.unitBitsEquiv line 253
  20. lemma OAI.ThorpNine.Dense.Thorp.relabeled_single_cycle_mean line 259
  21. def OAI.ThorpNine.Dense.Thorp.CycleColoring.projectSharedCycle line 273
  22. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.projectSharedCycle_injective line 286
  23. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.card_alternating_cycles_le_shared line 294
  24. def OAI.ThorpNine.Dense.Thorp.PairRouting.sharedPairs line 304
  25. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.alternatingCycles_le_sharedSelected line 307
  26. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sharedPairs_card_twice_le line 315
  27. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.labelSet_switched line 325
  28. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sharedPairs_switched line 332
  29. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.node_cycle_mean line 342
  30. lemma OAI.ThorpNine.Dense.Thorp.exp_secant line 383
  31. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_exp_bounded line 396
  32. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.node_cycle_mgf line 414
  33. lemma OAI.ThorpNine.Dense.Thorp.shared_pair_mgf line 435
  34. lemma OAI.ThorpNine.Dense.Thorp.prod_blockMarks line 487
  35. lemma OAI.ThorpNine.Dense.Thorp.subset_parallel_inverse line 502
  36. lemma OAI.ThorpNine.Dense.Thorp.parallel_inverse_cylinder line 520
  37. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.node_cycle_mean_one_fresh line 560
  38. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.node_cycle_mgf_fixed_input line 579
  39. def OAI.ThorpNine.Dense.Thorp.sharedLevel line 604
  40. def OAI.ThorpNine.Dense.Thorp.denseLevelCoefficient line 616
  41. lemma OAI.ThorpNine.Dense.Thorp.denseLevelCoefficient_nonneg line 619
  42. lemma OAI.ThorpNine.Dense.Thorp.palindrome_level_dense_conditional line 625
  43. def OAI.ThorpNine.Dense.Thorp.pairCoords line 670
  44. def OAI.ThorpNine.Dense.Thorp.gridPairs line 677
  45. def OAI.ThorpNine.Dense.Thorp.gridShared line 681
  46. lemma OAI.ThorpNine.Dense.Thorp.gridPairs_eq line 684
  47. lemma OAI.ThorpNine.Dense.Thorp.gridShared_zero line 701
  48. lemma OAI.ThorpNine.Dense.Thorp.gridShared_step line 730
  49. lemma OAI.ThorpNine.Dense.Thorp.butterfly_false line 747
  50. lemma OAI.ThorpNine.Dense.Thorp.inverseButterflyMarks_false line 764
  51. lemma OAI.ThorpNine.Dense.Thorp.sharedLevel_partial_marks line 771
  52. lemma OAI.ThorpNine.Dense.Thorp.partial_input_parallel line 794
  53. lemma OAI.ThorpNine.Dense.Thorp.partial_marks_parallel line 816
  54. lemma OAI.ThorpNine.Dense.Thorp.cylinder_image_equiv_bound line 827
  55. def OAI.ThorpNine.Dense.Thorp.suffixMarks line 837
  56. def OAI.ThorpNine.Dense.Thorp.sharedPartnerMean line 840
  57. lemma OAI.ThorpNine.Dense.Thorp.blockMarks_image_equiv line 844
  58. def OAI.ThorpNine.Dense.Thorp.pairReorder line 858
  59. lemma OAI.ThorpNine.Dense.Thorp.pairCoords_reorder line 864
  60. lemma OAI.ThorpNine.Dense.Thorp.partial_grid_mgf line 867