OAI/NumberTheory/Jacobsthal/Probability/ActualCouplingUpdates.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.MaximalCoupling.common line 26
  2. def OAI.Erdos970.Erdos970Dependency.MaximalCoupling.residual line 27
  3. def OAI.Erdos970.Erdos970Dependency.MaximalCoupling.leftRemainder line 28
  4. def OAI.Erdos970.Erdos970Dependency.MaximalCoupling.rightRemainder line 29
  5. def OAI.Erdos970.Erdos970Dependency.MaximalCoupling.matrix line 31
  6. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.common_nonneg line 36
  7. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.leftRemainder_nonneg line 40
  8. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.rightRemainder_nonneg line 43
  9. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.sum_leftRemainder line 46
  10. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.sum_rightRemainder line 48
  11. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.residual_nonneg line 51
  12. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.leftRemainder_zero line 55
  13. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.rightRemainder_zero line 60
  14. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.remainder_product_self line 68
  15. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.matrix_nonneg line 74
  16. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.row_sum line 83
  17. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.column_sum line 100
  18. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.matrix_diagonal line 117
  19. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.total_mass line 120
  20. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.mismatch_mass line 123
  21. theorem OAI.Erdos970.Erdos970Dependency.MaximalCoupling.exists_coupling line 135
  22. def OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.conditional line 156
  23. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.conditional_apply line 168
  24. instance OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.conditional_isMarkov line 171
  25. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.weighted_conditional line 184
  26. def OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.labelMass line 196
  27. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.labelMass_measurable line 199
  28. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.labelMass_nonneg line 204
  29. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.conditional_map_label line 207
  30. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.labelMass_sum line 225
  31. theorem OAI.Erdos970.NumberTheoryLean.KernelBinConditioning.conditional_mixture line 234
  32. def OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight line 267
  33. def OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.errorMass line 270
  34. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_measurable line 273
  35. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_joint_measurable line 290
  36. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_nonnegative line 300
  37. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_row line 303
  38. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_column line 306
  39. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_total line 309
  40. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_row_ofReal line 312
  41. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_column_ofReal line 317
  42. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_total_ofReal line 322
  43. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_le_left line 328
  44. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_le_right line 332
  45. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_zero_left line 336
  46. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_zero_right line 341
  47. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingWeights.weight_mismatch line 346
  48. def OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.component line 367
  49. instance OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.component_isSFinite line 372
  50. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.component_apply line 378
  51. def OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.coupled line 385
  52. instance OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.coupled_isSFinite line 388
  53. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.coupled_apply_set line 392
  54. instance OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.coupled_isMarkov line 403
  55. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.coupled_map_fst line 411
  56. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLift.coupled_map_snd line 423
  57. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLabels.component_labels line 455
  58. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLabels.coupled_labels line 466
  59. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLabels.coupled_mismatch line 474
  60. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLabels.errorMass_le_l1 line 501
  61. theorem OAI.Erdos970.NumberTheoryLean.KernelCouplingLabels.coupled_mismatch_le_l1 line 513
  62. abbrev OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.JointState line 532
  63. def OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.primeLabel line 535
  64. def OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.continuousLabel line 539
  65. theorem OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.primeLabel_measurable line 542
  66. theorem OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.continuousLabel_measurable line 545
  67. def OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.primeParent line 548
  68. def OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.continuousParent line 551
  69. instance OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.primeParent_isMarkov line 555
  70. instance OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.continuousParent_isMarkov line 558
  71. def OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.jointKernel line 565
  72. instance OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.jointKernel_isMarkov line 574
  73. theorem OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.jointKernel_left line 579
  74. theorem OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.jointKernel_right line 586
  75. theorem OAI.Erdos970.NumberTheoryLean.ActualProcessCoupling.jointKernel_mismatch_bound line 593
  76. def OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.continuousSupported line 619
  77. def OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.badRatio line 623
  78. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.badRatio_measurable line 625
  79. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.unsupported_eq line 628
  80. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.continuousSupported_measurable line 633
  81. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.continuous_supported line 639
  82. def OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.matchedOutcome line 657
  83. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.labels_match_outcomes line 662
  84. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.joint_continuous_supported line 688
  85. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingSupport.joint_matching_control line 695
  86. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.map_power_of_step line 723
  87. instance OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointKernel_pow_markov line 753
  88. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.joint_power_left line 764
  89. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.joint_power_right line 771
  90. def OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointPathLaw line 777
  91. instance OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointPathLaw_probability line 780
  92. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointPathLaw_prime line 785
  93. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointPathLaw_continuous line 789
  94. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointPathLaw_stage line 794
  95. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingFinite.jointPathLaw_prime_exit line 801
  96. def OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.liftPredicate line 827
  97. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.liftPredicate_measurable line 830
  98. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.complete_ae line 834
  99. def OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.primeFollows line 843
  100. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.prime_follows line 847
  101. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.side_set_measurable line 855
  102. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.stateKernel_side line 858
  103. def OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.continuousFollows line 872
  104. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.continuousFollows_measurable line 875
  105. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.costKernel_follows line 880
  106. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.continuous_follows line 888
  107. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.joint_follows line 896
  108. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.prime_step_gap line 912
  109. theorem OAI.Erdos970.NumberTheoryLean.ActualCouplingUpdates.matched_live_update line 920