OAI/Dynamics/ConditionalShuffle/Disintegration.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Revealed.outside line 13
  2. def OAI.Revealed.freeLabel line 15
  3. lemma OAI.Revealed.freeLabel_injective line 17
  4. def OAI.Revealed.imageRank line 21
  5. def OAI.Revealed.freeRank line 28
  6. def OAI.Revealed.layoutPath line 33
  7. abbrev OAI.Revealed.Environment line 38
  8. def OAI.Revealed.outsidePaths line 40
  9. def OAI.Revealed.slotPermutation line 44
  10. def OAI.Revealed.environmentMass line 48
  11. def OAI.Revealed.conditionalLaw line 51
  12. def OAI.Revealed.expectedTV line 57
  13. def OAI.Revealed.worstConditionalTV line 62
  14. def OAI.Revealed.twoHalfL line 65
  15. def OAI.Revealed.twoHalfP line 67
  16. def OAI.Revealed.twoHalfC line 69
  17. def OAI.Revealed.twoHalfB line 73
  18. def OAI.Thorp.Conditional.exposedPath line 80
  19. lemma OAI.Thorp.Conditional.exposedPath_last line 85
  20. lemma OAI.Thorp.Conditional.exposedPath_snoc line 91
  21. theorem OAI.Thorp.Conditional.flow_path_joint_identity line 97
  22. theorem OAI.Thorp.Conditional.halfDensity_after_step_sixteen line 154

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Energy.lean:12 (same declaration text).

  23. theorem OAI.Thorp.Conditional.expectedNoise_dimension_sixteen line 171

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Energy.lean:29 (same declaration text).

  24. theorem OAI.Thorp.Conditional.expectedNoise_bound_sixteen line 210

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Energy.lean:68 (same declaration text).

  25. lemma OAI.Thorp.Conditional.sixteen_density_geometric_choice line 222
  26. theorem OAI.Thorp.Conditional.expectedEnergy_decay_sixteen line 229

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Energy.lean:80 (same declaration text).

  27. theorem OAI.Thorp.Conditional.expectedEnergy_400 line 243
  28. theorem OAI.Thorp.Conditional.centeredPoint_energy_400 line 258
  29. def OAI.Thorp.Fourier.realProduct line 271
  30. lemma OAI.Thorp.Fourier.realProduct_nonneg line 275
  31. lemma OAI.Thorp.Fourier.realProduct_sum line 281
  32. lemma OAI.Thorp.Fourier.realConv_character line 287
  33. lemma OAI.Thorp.Fourier.realProduct_character_bound line 304
  34. lemma OAI.Thorp.Fourier.realProduct_transform_norm line 315
  35. lemma OAI.Thorp.Fourier.realProduct_hsSq line 331
  36. lemma OAI.Thorp.Fourier.Family.eight_sequence_transform_bound line 342
  37. lemma OAI.Thorp.Fourier.centered_probability_trivial line 377
  38. lemma OAI.Thorp.Fourier.centered_probability_character line 387
  39. theorem OAI.Thorp.Specht.permutation_eight_sequence_bound line 401
  40. theorem OAI.Thorp.Conditional.tagged_path_deviation_identity line 467
  41. theorem OAI.Thorp.Conditional.tagged_path_deviation_bound line 494
  42. def OAI.Thorp.Conditional.avoid line 513
  43. lemma OAI.Thorp.Conditional.avoid_exposed line 515
  44. lemma OAI.Thorp.Conditional.avoid_perm line 518
  45. lemma OAI.Thorp.Conditional.avoid_equiv_left line 522
  46. lemma OAI.Thorp.Conditional.avoid_equiv_right line 527
  47. lemma OAI.Thorp.Conditional.freeCount_avoid_equiv line 532
  48. def OAI.Thorp.Conditional.pathComplete line 542
  49. lemma OAI.Thorp.Conditional.pathComplete_bound line 548
  50. lemma OAI.Thorp.Conditional.exposedPath_comp line 568
  51. lemma OAI.Thorp.Conditional.pathComplete_equiv line 585
  52. lemma OAI.Thorp.Conditional.uniform_path_completion line 601
  53. def OAI.Thorp.Conditional.splitPath line 617
  54. def OAI.Thorp.Conditional.splitTuple line 621
  55. lemma OAI.Thorp.Conditional.splitTuple_snoc line 625
  56. lemma OAI.Thorp.Conditional.splitPath_last line 631
  57. lemma OAI.Thorp.Conditional.splitPath_completion_error line 640
  58. lemma OAI.Thorp.Conditional.uniform_splitTuple_completion line 703
  59. theorem OAI.Thorp.Conditional.splitTuple_test_400 line 723
  60. theorem OAI.Thorp.Conditional.splitTuple_joint_tv_400 line 786
  61. lemma OAI.Revealed.Split.perm_preserves_right line 813
  62. def OAI.Revealed.Split.rightPart line 821
  63. lemma OAI.Revealed.Split.rightPart_spec line 839
  64. def OAI.Revealed.Split.relative line 842
  65. lemma OAI.Revealed.Split.relative_spec line 845
  66. lemma OAI.Revealed.Split.relative_self line 850
  67. lemma OAI.Revealed.Split.relative_unique line 856
  68. lemma OAI.Revealed.Split.relative_factor line 863
  69. lemma OAI.Revealed.Split.relative_pre line 870
  70. lemma OAI.Revealed.Split.relative_post line 876
  71. abbrev OAI.Revealed.Split.Outside line 882
  72. def OAI.Revealed.Split.outside line 884
  73. def OAI.Revealed.Split.sectionFrame line 886
  74. lemma OAI.Revealed.Split.sectionFrame_spec line 888
  75. lemma OAI.Revealed.Split.outside_sectionFrame line 891
  76. lemma OAI.Revealed.Split.outside_pre line 896
  77. def OAI.Revealed.Split.assignment line 900
  78. lemma OAI.Revealed.Split.assignment_factor line 903
  79. lemma OAI.Revealed.Split.assignment_sectionFrame line 907
  80. lemma OAI.Revealed.Split.assignment_pre line 912
  81. def OAI.Revealed.Split.nextOutside line 917
  82. def OAI.Revealed.Split.increment line 920
  83. lemma OAI.Revealed.Split.outside_post line 923
  84. lemma OAI.Revealed.Split.assignment_post line 929
  85. def OAI.Revealed.Split.frameFor line 941
  86. lemma OAI.Revealed.Split.frameFor_outside line 944
  87. def OAI.Revealed.Split.indexRight line 949
  88. lemma OAI.Revealed.Split.indexRight_apply line 952
  89. lemma OAI.Revealed.Split.indexRight_assignment line 955
  90. lemma OAI.Revealed.Split.indexRight_tuple line 960
  91. lemma OAI.Thorp.Conditional.mean_perm_comp line 976
  92. theorem OAI.Thorp.Conditional.assignmentTuple_test_400 line 982
  93. def OAI.Revealed.Disintegration.marginal line 1021
  94. def OAI.Revealed.Disintegration.conditional line 1023
  95. lemma OAI.Revealed.Disintegration.marginal_nonneg line 1026
  96. lemma OAI.Revealed.Disintegration.point_le_marginal line 1032
  97. lemma OAI.Revealed.Disintegration.conditional_nonneg line 1038
  98. lemma OAI.Revealed.Disintegration.conditional_sum line 1045
  99. lemma OAI.Revealed.Disintegration.marginal_mul_conditional line 1053
  100. lemma OAI.Revealed.Disintegration.marginal_sum line 1061
  101. lemma OAI.Revealed.Disintegration.marginal_fairMass line 1065
  102. lemma OAI.Revealed.Disintegration.fairMass_prod line 1077
  103. lemma OAI.Revealed.Disintegration.tv_joint_scaled line 1091
  104. lemma OAI.Revealed.Disintegration.average_tv_eq line 1102
  105. lemma OAI.Revealed.Disintegration.push_preserve_first line 1117
  106. lemma OAI.Revealed.Disintegration.marginal_mul_push line 1124
  107. lemma OAI.Revealed.Disintegration.projection_tv_eq line 1134
  108. lemma OAI.Revealed.Disintegration.conditional_projection_le_of_test line 1143
  109. def OAI.Thorp.Conditional.frameJoint line 1171
  110. def OAI.Thorp.Conditional.frameKernel line 1176
  111. lemma OAI.Thorp.Conditional.frameJoint_nonneg line 1180
  112. lemma OAI.Thorp.Conditional.frameKernel_nonneg line 1183
  113. lemma OAI.Thorp.Conditional.frameKernel_sum line 1187
  114. lemma OAI.Thorp.Conditional.frameKernel_tuple_bound line 1191
  115. theorem OAI.Thorp.Conditional.frameKernel_marginal_400 line 1205