OAI/Probability/SKRatio/FiniteChain/DiscreteDistanceNonneg.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKRatio.discreteDistance_nonneg line 14
  2. theorem OAI.SKRatio.discreteDistance_le_one line 18
  3. theorem OAI.SKRatio.discreteDistance_antitone line 26
  4. theorem OAI.SKRatio.exists_geometric_bound line 41
  5. theorem OAI.SKRatio.exists_mixing_time line 48
  6. theorem OAI.SKRatio.mixingTime_spec line 55
  7. theorem OAI.SKRatio.mixingTime_le_of_distance_le line 59
  8. theorem OAI.SKRatio.mixingTime_le_iff line 62
  9. theorem OAI.SKRatio.lt_mixingTime_of_lt_distance line 69
  10. theorem OAI.SKRatio.discreteDistance_zero_lower line 73
  11. theorem OAI.SKRatio.denominator_eventually_positive line 94
  12. theorem OAI.SKRatio.mixing_ratio_bound line 104
  13. theorem OAI.SKRatio.continuous_coupling line 136
  14. theorem OAI.SKRatio.continuous_hamiltonian line 141
  15. theorem OAI.SKRatio.continuous_weight line 146
  16. theorem OAI.SKRatio.continuous_partition line 151
  17. theorem OAI.SKRatio.continuous_mass line 156
  18. theorem OAI.SKRatio.continuous_siteKernel line 161
  19. theorem OAI.SKRatio.continuous_transition line 172
  20. theorem OAI.SKRatio.continuous_transition_pow line 180
  21. theorem OAI.SKRatio.continuous_discreteDistance line 188
  22. theorem OAI.SKRatio.measurable_mixingTime line 199
  23. theorem OAI.SKRatio.measurableSet_ratio_event line 210