OAI/Probability/ThorpRouting/Casimir/ModifiedRoutingMoment.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Casimir.Thorp.modified_probability_zero_le line 10
  2. def OAI.ThorpNine.Casimir.Thorp.modifiedRoutingMoment line 33
  3. lemma OAI.ThorpNine.Casimir.Thorp.modifiedRoutingMoment_nonneg line 39
  4. lemma OAI.ThorpNine.Casimir.Thorp.modifiedRoutingMoment_zero line 45
  5. lemma OAI.ThorpNine.Casimir.Thorp.modified_pointwise_zero line 51
  6. lemma OAI.ThorpNine.Casimir.Thorp.modified_matches_step line 71
  7. lemma OAI.ThorpNine.Casimir.Thorp.modifiedRoutingMoment_step line 82
  8. lemma OAI.ThorpNine.Casimir.Thorp.modified_child_moment_product line 126
  9. lemma OAI.ThorpNine.Casimir.Thorp.modified_probability_step line 158
  10. lemma OAI.ThorpNine.Casimir.Thorp.modified_assignment_moment_bound line 176
  11. lemma OAI.ThorpNine.Casimir.Thorp.modified_child_power_product_bound line 216
  12. theorem OAI.ThorpNine.Casimir.Thorp.modified_pointwise_moment line 257
  13. lemma OAI.ThorpNine.Casimir.Thorp.modifiedRoutingMoment_sum line 321
  14. def OAI.ThorpNine.Casimir.Thorp.modifiedRowMoment line 343
  15. lemma OAI.ThorpNine.Casimir.Thorp.full_tuple_card line 348
  16. lemma OAI.ThorpNine.Casimir.Thorp.exception_card_le line 353
  17. def OAI.ThorpNine.Casimir.Thorp.modifiedNormalization line 356
  18. lemma OAI.ThorpNine.Casimir.Thorp.modifiedNormalization_pos line 360
  19. lemma OAI.ThorpNine.Casimir.Thorp.modified_normalization_identity line 363
  20. theorem OAI.ThorpNine.Casimir.Thorp.modified_row_density_moment line 377
  21. lemma OAI.ThorpNine.Casimir.Thorp.modified_total_cost_mgf line 394
  22. lemma OAI.ThorpNine.Casimir.Thorp.modifiedRowMoment_bound line 407
  23. lemma OAI.ThorpNine.Casimir.Thorp.log_factorial_upper line 420
  24. lemma OAI.ThorpNine.Casimir.Thorp.log_modifiedNormalization line 438
  25. lemma OAI.ThorpNine.Casimir.Thorp.log_modifiedNormalization_le line 448
  26. lemma OAI.ThorpNine.Casimir.Thorp.modified_moment_exponential line 460
  27. lemma OAI.ThorpNine.Casimir.Thorp.log_power_factorial_le line 471
  28. lemma OAI.ThorpNine.Casimir.Thorp.modified_moment_exception_bound line 482
  29. lemma OAI.ThorpNine.Casimir.Thorp.heightDecay_tendsto line 498
  30. def OAI.ThorpNine.Casimir.Thorp.modifiedOverhead line 510
  31. lemma OAI.ThorpNine.Casimir.Thorp.modifiedOverhead_tendsto line 513
  32. theorem OAI.ThorpNine.Casimir.Thorp.modified_arbitrarily_small_rate line 528
  33. def OAI.ThorpNine.Casimir.Thorp.DensityTransfer.applyKernel line 568
  34. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.applyKernel_apply line 572
  35. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.applyKernel_add line 576
  36. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.kernel_component_sq line 583
  37. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.schur_bound line 597
  38. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.hilbert_schmidt_family line 624
  39. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tail_density_pointwise line 648
  40. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tail_density_mean line 657
  41. def OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tailKernel line 663
  42. def OAI.ThorpNine.Casimir.Thorp.DensityTransfer.headKernel line 666
  43. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tail_add_head line 669
  44. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tailKernel_nonneg line 675
  45. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tailKernel_row line 680
  46. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.tailKernel_schur line 701
  47. lemma OAI.ThorpNine.Casimir.Thorp.DensityTransfer.headKernel_hs line 716
  48. theorem OAI.ThorpNine.Casimir.Thorp.DensityTransfer.multiplicity_amplification line 738
  49. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.tupleProbability_row_sum line 778
  50. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.tupleProbability_inverse line 792
  51. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.tupleProbability_equiv line 808
  52. lemma OAI.ThorpNine.Casimir.Thorp.PairRouting.tupleProbability_symmetric line 813
  53. lemma OAI.ThorpNine.Casimir.Thorp.palindromePerm_reverse line 823
  54. lemma OAI.ThorpNine.Casimir.Thorp.palindrome_kernel_symmetric line 828
  55. theorem OAI.ThorpNine.Casimir.Thorp.palindrome_density_transfer line 834