OAI/Probability/ThorpRouting/Tail/TailShapes.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThorpNine.Tail.Thorp.Specht.TailShapes line 11
  2. def OAI.ThorpNine.Tail.Thorp.Specht.tailShapePartition line 13
  3. lemma OAI.ThorpNine.Tail.Thorp.Specht.tailShapePartition_injective line 18
  4. lemma OAI.ThorpNine.Tail.Thorp.Specht.tail_shapes_count line 34
  5. lemma OAI.ThorpNine.Tail.Thorp.tail_preserving_pairSwitch line 42
  6. lemma OAI.ThorpNine.Tail.Thorp.pairSwitch_injective line 70
  7. def OAI.ThorpNine.Tail.Thorp.Specht.pairFiberEquiv line 81
  8. lemma OAI.ThorpNine.Tail.Thorp.Specht.pair_sum_taboid_zero line 102
  9. lemma OAI.ThorpNine.Tail.Thorp.Specht.pair_operator_tall_zero line 111
  10. lemma OAI.ThorpNine.Tail.Thorp.Specht.palindrome_tall_zero line 135
  11. lemma OAI.ThorpNine.Tail.Thorp.Specht.palindrome_tall_zero_general line 148
  12. lemma OAI.ThorpNine.Tail.Thorp.DimensionEstimates.twopow_tendsto line 163
  13. lemma OAI.ThorpNine.Tail.Thorp.DimensionEstimates.twopow_nat_tendsto line 166
  14. lemma OAI.ThorpNine.Tail.Thorp.DimensionEstimates.twopow_mul_eventually line 169
  15. lemma OAI.ThorpNine.Tail.Thorp.DimensionEstimates.exp_two_absorb line 174
  16. theorem OAI.ThorpNine.Tail.Thorp.Specht.exponential_dimension_spectral line 185
  17. theorem OAI.ThorpNine.Tail.Thorp.Specht.spectral_regimes line 252
  18. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.regularAbsoluteEvenTrace line 309
  19. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.MainStatement line 312
  20. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.mean_nonneg line 327
  21. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.mean_rpow_concave line 330
  22. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.act line 342
  23. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.act_nonneg line 345
  24. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.act_rpow_le line 350
  25. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.act_one_to_p line 358
  26. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.act_b_to_pb line 407
  27. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.kernel_pow_nonneg line 424
  28. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.kernel_pow_row line 435
  29. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.rowDensity line 446
  30. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.rowDensity_nonneg line 450
  31. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.rowDensity_succ line 454
  32. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.rowDensity_mean line 461
  33. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.rowDensity_moment_iter line 466
  34. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.rowDensity_second_moment line 493
  35. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.symmetric_kernel_smoothing line 515
  36. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.density_exponent_numeric line 547
  37. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.kernel line 559
  38. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.nonneg line 563
  39. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.row line 566
  40. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.inverse line 571
  41. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.col line 580
  42. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.mul line 585
  43. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.PermLaw.conjugate line 603
  44. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.mul_nonneg_entries line 621
  45. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.mul_row line 626
  46. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.mul_col line 633
  47. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.bound_mul_left line 640
  48. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.bound_mul_right line 649
  49. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sandwich_power line 657
  50. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.tuplePerm line 671
  51. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.tuplePerm_apply line 678
  52. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.tuplePerm_mul line 682
  53. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.tuplePerm_inverse line 688
  54. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.tupleProbability_kernel line 694
  55. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweepKernel_law line 706
  56. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflectedKernel_conjugate line 711
  57. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweepKernel_nonneg line 734
  58. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweepKernel_row line 737
  59. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweepKernel_col line 742
  60. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflected_nonneg line 747
  61. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflected_row line 752
  62. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflected_col line 756
  63. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflected_symmetric line 760
  64. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflected_moment line 763
  65. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.tuples_card line 779
  66. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.canonical_pointwise line 782
  67. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.both_pointwise line 795
  68. lemma OAI.ThorpNine.Tail.Thorp.StrongSmoothing.regular_trace_bound line 812
  69. theorem OAI.ThorpNine.Tail.Thorp.StrongSmoothing.strong_smoothing line 829
  70. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.mem_tailDiagram line 840
  71. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.tail_height line 854