OAI/Probability/ThorpRouting/Dense/PalindromeFamilyCost.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Dense.Thorp.familyEnd_two line 10
  2. lemma OAI.ThorpNine.Dense.Thorp.familyEnd_ge line 15
  3. def OAI.ThorpNine.Dense.Thorp.palindromeFamilyCost line 23
  4. lemma OAI.ThorpNine.Dense.Thorp.palindromeFamilyCost_adapted line 27
  5. theorem OAI.ThorpNine.Dense.Thorp.palindrome_family_mgf line 35
  6. lemma OAI.ThorpNine.Dense.Thorp.pow_four_ge line 71
  7. lemma OAI.ThorpNine.Dense.Thorp.sum_family_decay line 76
  8. lemma OAI.ThorpNine.Dense.Thorp.palindromeLevelCost_step_add line 101
  9. lemma OAI.ThorpNine.Dense.Thorp.palindromeLowCost_sum line 119
  10. lemma OAI.ThorpNine.Dense.Thorp.palindromeLowCost_slab line 132
  11. lemma OAI.ThorpNine.Dense.Thorp.palindromeCost_family line 139
  12. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_mul_sq_le line 154
  13. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_mul_exp_le line 160
  14. def OAI.ThorpNine.Dense.Thorp.heightDecay line 178
  15. lemma OAI.ThorpNine.Dense.Thorp.heightDecay_nonneg line 181
  16. lemma OAI.ThorpNine.Dense.Thorp.heightDecay_antitone line 185
  17. lemma OAI.ThorpNine.Dense.Thorp.palindrome_family_mgf_decay line 196
  18. theorem OAI.ThorpNine.Dense.Thorp.palindrome_high_mgf line 207
  19. lemma OAI.ThorpNine.Dense.Thorp.palindrome_high_full_mgf line 224
  20. theorem OAI.ThorpNine.Dense.Thorp.palindrome_cost_mgf_cutoff line 236
  21. lemma OAI.ThorpNine.Dense.Thorp.cutoffMass_le line 262
  22. lemma OAI.ThorpNine.Dense.Thorp.palindromeLowCost_le line 273
  23. theorem OAI.ThorpNine.Dense.Thorp.palindrome_cost_mgf_coarse line 277
  24. def OAI.ThorpNine.Dense.Thorp.momentBase line 314
  25. lemma OAI.ThorpNine.Dense.Thorp.momentBase_one_le line 316
  26. lemma OAI.ThorpNine.Dense.Thorp.momentBase_log line 319
  27. lemma OAI.ThorpNine.Dense.Thorp.momentBase_pow line 325
  28. lemma OAI.ThorpNine.Dense.Thorp.palindromeRowMoment_le_cost line 329
  29. theorem OAI.ThorpNine.Dense.Thorp.palindrome_row_moment_coarse line 346
  30. def OAI.ThorpNine.Dense.Thorp.densityCutoff line 352
  31. lemma OAI.ThorpNine.Dense.Thorp.log_small_density line 354
  32. lemma OAI.ThorpNine.Dense.Thorp.densityCutoff_bounds line 362
  33. lemma OAI.ThorpNine.Dense.Thorp.densityCutoff_decay line 376
  34. lemma OAI.ThorpNine.Dense.Thorp.densityCutoff_power line 388
  35. lemma OAI.ThorpNine.Dense.Thorp.densityCutoff_sparse line 409
  36. lemma OAI.ThorpNine.Dense.Thorp.momentBase_log_exact line 424
  37. lemma OAI.ThorpNine.Dense.Thorp.densityCutoff_le_height line 428
  38. def OAI.ThorpNine.Dense.Thorp.densityTailConstant line 445
  39. lemma OAI.ThorpNine.Dense.Thorp.densityTailConstant_nonneg line 448
  40. lemma OAI.ThorpNine.Dense.Thorp.heightDecay_cutoff line 452
  41. lemma OAI.ThorpNine.Dense.Thorp.sparse_low_algebra line 461
  42. lemma OAI.ThorpNine.Dense.Thorp.palindrome_row_moment_small line 470
  43. def OAI.ThorpNine.Dense.Thorp.densityConstant line 507
  44. lemma OAI.ThorpNine.Dense.Thorp.densityConstant_pos line 510
  45. theorem OAI.ThorpNine.Dense.Thorp.palindrome_row_moment_bound line 516
  46. lemma OAI.ThorpNine.Dense.Thorp.palindromeRowMoment_nonneg line 551
  47. theorem OAI.ThorpNine.Dense.Thorp.palindrome_log_row_moment line 558
  48. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.single_min_eq_within line 577
  49. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.single_rotationCharge_mean_bound line 595
  50. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.single_rotation_exp_bound line 618
  51. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.single_collection_rotation_lower line 643
  52. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.single_cycleSlots_weighted_moment line 659
  53. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.singleRootedEquiv line 695
  54. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.single_root_count line 723
  55. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.uniform_cycle_length_cap line 735
  56. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.law_reciprocal_summable line 762
  57. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.law_reciprocal_nonneg line 769
  58. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.law_reciprocal_le_one line 774
  59. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.reciprocal_values_bdd line 781
  60. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.reciprocal_le_h line 786
  61. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.subprob_reciprocal_le_h line 791