OAI/Probability/ThorpRouting/Tail/Representative.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.averageMap_self_trace line 14
  2. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.averageMap_scalar line 23
  3. theorem OAI.ThorpNine.Tail.Thorp.UnitaryFinite.coefficient_orthogonality line 34
  4. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.representative line 59
  5. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.representative_apply line 62
  6. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.orbit_sum line 66
  7. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.IsFixed line 86
  8. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.coefficient line 88
  9. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.coefficient_at line 92
  10. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.coefficient_inner line 107
  11. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.coefficient_action line 134
  12. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.normalizedCoefficient line 142
  13. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.normalizedCoefficient_inner line 145
  14. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.normalizedCoefficient_orthonormal line 162
  15. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.normalizedCoefficient_norm line 172
  16. def OAI.ThorpNine.Tail.Thorp.FiniteConvolution.conv line 188
  17. def OAI.ThorpNine.Tail.Thorp.FiniteConvolution.power line 189
  18. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.conv_nonneg line 193
  19. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.conv_pos_of line 196
  20. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.sum_conv line 203
  21. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.power_nonneg line 212
  22. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.sum_power line 218
  23. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.power_list_pos line 224
  24. lemma OAI.ThorpNine.Tail.Thorp.FiniteConvolution.power_pos_mono line 233
  25. theorem OAI.ThorpNine.Tail.Thorp.FiniteConvolution.exists_positive_power line 240
  26. structure OAI.ThorpNine.Tail.Thorp.FiniteConvolution.Minorant line 255
  27. def OAI.ThorpNine.Tail.Thorp.FiniteConvolution.minorant line 262
  28. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.continuousRepresentation_apply line 287
  29. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.unitary_norm line 291
  30. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.continuousRepresentation_norm_le line 296
  31. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.continuousRepresentation_adjoint line 303
  32. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weightedOperator line 311
  33. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weightedOperator_norm_le line 314
  34. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weightedOperator_symmetric line 322
  35. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.uniformOperator line 332
  36. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.uniformOperator_symmetric line 335
  37. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.uniformOperator_left line 338
  38. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.uniformOperator_right line 345
  39. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.uniformOperator_idempotent line 352
  40. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.uniformOperator_projection line 361
  41. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weighted_uniform_left line 365
  42. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weighted_uniform_right line 372
  43. theorem OAI.ThorpNine.Tail.Thorp.UnitaryFinite.doeblin_off_invariants line 379
  44. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weightedOperator_conv line 414
  45. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.weightedOperator_power line 427
  46. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.off_invariants_pow line 433
  47. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.minorantGap line 447
  48. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.minorantGap_pos line 451
  49. lemma OAI.ThorpNine.Tail.Thorp.UnitaryFinite.minorantGap_lt_one line 460
  50. theorem OAI.ThorpNine.Tail.Thorp.UnitaryFinite.norm_off_invariants_le_gap line 464
  51. def OAI.ThorpNine.Tail.Thorp.butterflyIdentity line 494
  52. lemma OAI.ThorpNine.Tail.Thorp.pairSwitch_false line 498
  53. lemma OAI.ThorpNine.Tail.Thorp.childLift_one line 504
  54. lemma OAI.ThorpNine.Tail.Thorp.butterflyIdentity_perm line 508
  55. def OAI.ThorpNine.Tail.Thorp.childInjection line 513
  56. lemma OAI.ThorpNine.Tail.Thorp.childInjection_swap line 522
  57. lemma OAI.ThorpNine.Tail.Thorp.pairSwitch_single line 542
  58. theorem OAI.ThorpNine.Tail.Thorp.butterfly_generates line 555
  59. lemma OAI.ThorpNine.Tail.Thorp.butterfly_closure line 595
  60. def OAI.ThorpNine.Tail.Thorp.sampleLaw line 600
  61. lemma OAI.ThorpNine.Tail.Thorp.sampleLaw_nonneg line 604
  62. lemma OAI.ThorpNine.Tail.Thorp.sampleLaw_sum line 607
  63. lemma OAI.ThorpNine.Tail.Thorp.sampleLaw_pos_iff line 613
  64. lemma OAI.ThorpNine.Tail.Thorp.sampleLaw_equiv line 624
  65. lemma OAI.ThorpNine.Tail.Thorp.sampleLaw_inverse line 632
  66. lemma OAI.ThorpNine.Tail.Thorp.sampleLaw_symmetric line 639
  67. lemma OAI.ThorpNine.Tail.Thorp.palindrome_identity line 650
  68. lemma OAI.ThorpNine.Tail.Thorp.palindrome_range_contains_butterfly line 655
  69. lemma OAI.ThorpNine.Tail.Thorp.palindrome_support_generates line 663
  70. def OAI.ThorpNine.Tail.Thorp.palindromeMinorant line 670
  71. def OAI.ThorpNine.Tail.Thorp.blockGap line 675
  72. lemma OAI.ThorpNine.Tail.Thorp.blockGap_pos line 677
  73. lemma OAI.ThorpNine.Tail.Thorp.blockGap_lt_one line 678
  74. theorem OAI.ThorpNine.Tail.Thorp.palindrome_off_invariants_gap line 680
  75. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.orthogonal_sum_norm_sq line 696
  76. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.projection_inner_zero line 709
  77. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.projection_sandwich_norm line 716
  78. theorem OAI.ThorpNine.Tail.Thorp.CommutingBlocks.resolution_norm_bound line 725
  79. theorem OAI.ThorpNine.Tail.Thorp.CommutingBlocks.sector_sandwich_le line 753
  80. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.resolution_commute line 775
  81. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.resolution_sum_mul line 782
  82. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.resolution_truncated_norm line 792
  83. theorem OAI.ThorpNine.Tail.Thorp.CommutingBlocks.resolution_exception_bound line 807
  84. def OAI.ThorpNine.Tail.Thorp.CommutingBlocks.choice line 841
  85. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.choice_commute line 846
  86. def OAI.ThorpNine.Tail.Thorp.CommutingBlocks.sector line 855
  87. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.sector_insert line 859
  88. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.sector_congr line 864
  89. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.sector_factor_commute line 871
  90. lemma OAI.ThorpNine.Tail.Thorp.CommutingBlocks.sector_projection line 876