OAI/Probability/SKCutoff/Denominator.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Finite heat-bath mixing and positivity of the SK cutoff denominator.

  1. def OAI.SKCutoff.siteKernel line 14
  2. def OAI.SKCutoff.transition line 21
  3. def OAI.SKCutoff.totalVariation line 24
  4. def OAI.SKCutoff.discreteDistance line 27
  5. def OAI.SKCutoff.mixingTime line 31
  6. def OAI.SKCutoff.ratioEvent line 34
  7. theorem OAI.SKCutoff.flip_same line 39
  8. theorem OAI.SKCutoff.flip_other line 42
  9. theorem OAI.SKCutoff.flip_flip line 46
  10. theorem OAI.SKCutoff.flip_ne line 52
  11. theorem OAI.SKCutoff.weight_pos line 58
  12. theorem OAI.SKCutoff.partition_pos line 61
  13. theorem OAI.SKCutoff.mass_pos line 64
  14. theorem OAI.SKCutoff.mass_nonneg line 67
  15. theorem OAI.SKCutoff.sum_mass line 70
  16. theorem OAI.SKCutoff.mass_le_one line 74
  17. instance OAI.SKCutoff.disorderLaw_probability line 79
  18. theorem OAI.SKCutoff.siteKernel_nonneg line 83
  19. theorem OAI.SKCutoff.sum_siteKernel line 90
  20. theorem OAI.SKCutoff.siteKernel_pos_self line 97
  21. theorem OAI.SKCutoff.siteKernel_pos_flip line 103
  22. theorem OAI.SKCutoff.siteKernel_detailed_balance line 108
  23. theorem OAI.SKCutoff.transition_eq line 126
  24. theorem OAI.SKCutoff.transition_eq_zero line 130
  25. theorem OAI.SKCutoff.transition_stochastic line 134
  26. theorem OAI.SKCutoff.transition_nonneg line 151
  27. theorem OAI.SKCutoff.transition_power_stochastic line 154
  28. theorem OAI.SKCutoff.transition_power_nonneg line 158
  29. theorem OAI.SKCutoff.transition_detailed_balance line 161
  30. theorem OAI.SKCutoff.mass_stationary line 177
  31. theorem OAI.SKCutoff.mass_stationary_power line 189
  32. theorem OAI.SKCutoff.transition_pos_of_fiber line 196
  33. theorem OAI.SKCutoff.eq_or_eq_flip line 208
  34. def OAI.SKCutoff.updatePrefix line 224
  35. theorem OAI.SKCutoff.updatePrefix_zero line 227
  36. theorem OAI.SKCutoff.updatePrefix_all line 231
  37. theorem OAI.SKCutoff.updatePrefix_step line 235
  38. theorem OAI.SKCutoff.transition_power_positive line 248
  39. theorem OAI.SKCutoff.totalVariation_nonneg line 270
  40. theorem OAI.SKCutoff.totalVariation_le_one line 273
  41. theorem OAI.SKCutoff.totalVariation_contract line 284
  42. theorem OAI.SKCutoff.totalVariation_power_bound line 323
  43. theorem OAI.SKCutoff.mixing_set_nonempty line 354
  44. theorem OAI.SKCutoff.mixingTime_spec line 387
  45. theorem OAI.SKCutoff.mixingTime_le line 391
  46. theorem OAI.SKCutoff.totalVariation_dirac line 395
  47. theorem OAI.SKCutoff.discreteDistance_zero line 414
  48. theorem OAI.SKCutoff.discreteDistance_zero_lower line 428
  49. theorem OAI.SKCutoff.denominator_positive line 448
  50. theorem OAI.SKCutoff.denominator_pos_eventually line 457
  51. theorem OAI.SKCutoff.discreteDistance_antitone line 464
  52. theorem OAI.SKCutoff.mixingTime_le_iff line 481
  53. theorem OAI.SKCutoff.discreteDistance_tendsto_zero line 488
  54. theorem OAI.SKCutoff.continuous_coupling line 502
  55. theorem OAI.SKCutoff.continuous_weight line 507
  56. theorem OAI.SKCutoff.continuous_partition line 512
  57. theorem OAI.SKCutoff.continuous_mass line 517
  58. theorem OAI.SKCutoff.continuous_siteKernel line 521
  59. theorem OAI.SKCutoff.continuous_transition line 534
  60. theorem OAI.SKCutoff.continuous_transition_power line 542
  61. theorem OAI.SKCutoff.continuous_discreteDistance line 552
  62. theorem OAI.SKCutoff.measurable_mixingTime line 566
  63. theorem OAI.SKCutoff.measurableSet_ratioEvent line 578