OAI/Probability/ThorpRouting/Dense/Main.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Dense.Thorp.sharedPartnerMean_nonneg line 11
  2. lemma OAI.ThorpNine.Dense.Thorp.sum_suffix_pair_counts line 16
  3. lemma OAI.ThorpNine.Dense.Thorp.sharedPartnerMean_twice_le line 24
  4. lemma OAI.ThorpNine.Dense.Thorp.palindrome_level_dense_mgf line 47
  5. lemma OAI.ThorpNine.Dense.Thorp.cardSplit_snd_apply line 72
  6. def OAI.ThorpNine.Dense.Thorp.PairSeparated line 85
  7. lemma OAI.ThorpNine.Dense.Thorp.PairSeparated.unique line 88
  8. lemma OAI.ThorpNine.Dense.Thorp.PairSeparated.not_reverse line 99
  9. lemma OAI.ThorpNine.Dense.Thorp.pairSeparated_split_iff line 112
  10. abbrev OAI.ThorpNine.Dense.Thorp.SeparatedPair line 145
  11. def OAI.ThorpNine.Dense.Thorp.separatedCount line 148
  12. lemma OAI.ThorpNine.Dense.Thorp.separated_budget_strong line 152
  13. lemma OAI.ThorpNine.Dense.Thorp.separated_budget line 198
  14. lemma OAI.ThorpNine.Dense.Thorp.mem_suffixMarks line 202
  15. lemma OAI.ThorpNine.Dense.Thorp.separatedCount_eq line 206
  16. def OAI.ThorpNine.Dense.Thorp.partnerMean line 253
  17. lemma OAI.ThorpNine.Dense.Thorp.partnerMean_nonneg line 256
  18. lemma OAI.ThorpNine.Dense.Thorp.partnerMean_eq line 261
  19. lemma OAI.ThorpNine.Dense.Thorp.partnerMean_twice_le line 269
  20. lemma OAI.ThorpNine.Dense.Thorp.partnerMean_rate line 277
  21. lemma OAI.ThorpNine.Dense.Thorp.partnerMean_budget line 285
  22. def OAI.ThorpNine.Dense.Thorp.partnerAllocation line 298
  23. lemma OAI.ThorpNine.Dense.Thorp.partnerAllocation_admissible line 301
  24. lemma OAI.ThorpNine.Dense.Thorp.partner_weighted_sum_le line 330
  25. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_rpow_le line 350
  26. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_exp_scale line 362
  27. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_exp_sum_le line 377
  28. lemma OAI.ThorpNine.Dense.Thorp.dense_coefficient_hasDerivAt line 430
  29. lemma OAI.ThorpNine.Dense.Thorp.dense_coefficient_small line 440
  30. lemma OAI.ThorpNine.Dense.Thorp.palindrome_level_dense_mgf_all line 462
  31. lemma OAI.ThorpNine.Dense.Thorp.palindrome_low_dense_mgf line 474
  32. lemma OAI.ThorpNine.Dense.Thorp.heightDecay_tendsto line 521
  33. lemma OAI.ThorpNine.Dense.Thorp.heightDecay_exists line 532
  34. lemma OAI.ThorpNine.Dense.Thorp.palindrome_high_exp_mgf line 539
  35. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.harmonic_le_h line 564
  36. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.harmonic_lower line 603
  37. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.h_log_lower line 610
  38. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.unusedTail line 616
  39. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.unusedTail_nonneg line 619
  40. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.unusedTail_lower line 623
  41. lemma OAI.ThorpNine.Dense.Thorp.partnerMean_budget_strong line 649
  42. lemma OAI.ThorpNine.Dense.Thorp.partnerAllocation_range_budget line 664
  43. lemma OAI.ThorpNine.Dense.Thorp.dyadic_weights_hasSum line 677
  44. def OAI.ThorpNine.Dense.Thorp.augmentedAllocation line 688
  45. lemma OAI.ThorpNine.Dense.Thorp.augmentedAllocation_bounds line 691
  46. lemma OAI.ThorpNine.Dense.Thorp.augmentedAllocation_admissible line 698
  47. lemma OAI.ThorpNine.Dense.Thorp.partner_weighted_sum_gap line 721
  48. lemma OAI.ThorpNine.Dense.Thorp.palindrome_low_dense_mgf_gap line 771
  49. lemma OAI.ThorpNine.Dense.Thorp.palindrome_dense_mgf line 818
  50. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder line 878
  51. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_zero line 881
  52. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_step line 884
  53. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.log_increment_mul_monotone line 893
  54. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_increment_antitone line 925
  55. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_upper line 931
  56. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_sum line 947
  57. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_step_bound line 954
  58. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_average_antitone line 964
  59. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_difference_bound line 976
  60. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.stirlingRemainder_dyadic line 1000
  61. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.factorial_error_identity line 1017
  62. lemma OAI.ThorpNine.Dense.Thorp.DenseTruncation.normalization_le line 1049
  63. theorem OAI.ThorpNine.Dense.Thorp.DenseTruncation.dense_truncation line 1082