OAI/Probability/ThorpRouting/Adaptive/ModifiedRoutingMoment.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Adaptive.Thorp.modifiedRoutingMoment line 10
  2. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedRoutingMoment_nonneg line 16
  3. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedRoutingMoment_zero line 22
  4. lemma OAI.ThorpNine.Adaptive.Thorp.modified_pointwise_zero line 28
  5. lemma OAI.ThorpNine.Adaptive.Thorp.modified_matches_step line 48
  6. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedRoutingMoment_step line 59
  7. lemma OAI.ThorpNine.Adaptive.Thorp.modified_child_moment_product line 103
  8. lemma OAI.ThorpNine.Adaptive.Thorp.modified_probability_step line 135
  9. lemma OAI.ThorpNine.Adaptive.Thorp.modified_assignment_moment_bound line 153
  10. lemma OAI.ThorpNine.Adaptive.Thorp.modified_child_power_product_bound line 193
  11. theorem OAI.ThorpNine.Adaptive.Thorp.modified_pointwise_moment line 234
  12. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedRoutingMoment_sum line 298
  13. def OAI.ThorpNine.Adaptive.Thorp.modifiedRowMoment line 320
  14. lemma OAI.ThorpNine.Adaptive.Thorp.full_tuple_card line 325
  15. lemma OAI.ThorpNine.Adaptive.Thorp.exception_card_le line 330
  16. def OAI.ThorpNine.Adaptive.Thorp.modifiedNormalization line 333
  17. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedNormalization_pos line 337
  18. lemma OAI.ThorpNine.Adaptive.Thorp.modified_normalization_identity line 340
  19. theorem OAI.ThorpNine.Adaptive.Thorp.modified_row_density_moment line 354
  20. lemma OAI.ThorpNine.Adaptive.Thorp.modified_total_cost_mgf line 371
  21. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedRowMoment_bound line 384
  22. lemma OAI.ThorpNine.Adaptive.Thorp.log_factorial_upper line 397
  23. lemma OAI.ThorpNine.Adaptive.Thorp.log_modifiedNormalization line 415
  24. lemma OAI.ThorpNine.Adaptive.Thorp.log_modifiedNormalization_le line 425
  25. lemma OAI.ThorpNine.Adaptive.Thorp.modified_moment_exponential line 437
  26. lemma OAI.ThorpNine.Adaptive.Thorp.log_power_factorial_le line 448
  27. lemma OAI.ThorpNine.Adaptive.Thorp.modified_moment_exception_bound line 459
  28. lemma OAI.ThorpNine.Adaptive.Thorp.heightDecay_tendsto line 475
  29. def OAI.ThorpNine.Adaptive.Thorp.modifiedOverhead line 487
  30. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedOverhead_tendsto line 490
  31. theorem OAI.ThorpNine.Adaptive.Thorp.modified_arbitrarily_small_rate line 505
  32. def OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.applyKernel line 545
  33. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.applyKernel_apply line 549
  34. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.applyKernel_add line 553
  35. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.kernel_component_sq line 560
  36. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.schur_bound line 574
  37. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.hilbert_schmidt_family line 601
  38. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tail_density_pointwise line 625
  39. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tail_density_mean line 634
  40. def OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tailKernel line 640
  41. def OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.headKernel line 643
  42. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tail_add_head line 646
  43. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tailKernel_nonneg line 652
  44. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tailKernel_row line 657
  45. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.tailKernel_schur line 678
  46. lemma OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.headKernel_hs line 693
  47. theorem OAI.ThorpNine.Adaptive.Thorp.DensityTransfer.multiplicity_amplification line 715
  48. lemma OAI.ThorpNine.Adaptive.Thorp.PairRouting.tupleProbability_row_sum line 755
  49. lemma OAI.ThorpNine.Adaptive.Thorp.PairRouting.tupleProbability_inverse line 769
  50. lemma OAI.ThorpNine.Adaptive.Thorp.PairRouting.tupleProbability_equiv line 785
  51. lemma OAI.ThorpNine.Adaptive.Thorp.PairRouting.tupleProbability_symmetric line 790
  52. lemma OAI.ThorpNine.Adaptive.Thorp.palindromePerm_reverse line 800
  53. lemma OAI.ThorpNine.Adaptive.Thorp.palindrome_kernel_symmetric line 805
  54. theorem OAI.ThorpNine.Adaptive.Thorp.palindrome_density_transfer line 811
  55. def OAI.ThorpNine.Adaptive.Thorp.modifiedReverseCoins line 830
  56. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedReverseCoins_involutive line 838