OAI/Probability/SKRatio/FiniteChain/Spin.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatio.Spin line 12

    Also declared: ComparatorChallenges/SKRatio.lean:11 (same declaration text).

  2. abbrev OAI.SKRatio.Edge line 13

    Also declared: ComparatorChallenges/SKRatio.lean:12 (same declaration text).

  3. abbrev OAI.SKRatio.Disorder line 14

    Also declared: ComparatorChallenges/SKRatio.lean:13 (same declaration text).

  4. def OAI.SKRatio.spinValue line 16

    Also declared: ComparatorChallenges/SKRatio.lean:15 (same declaration text).

  5. def OAI.SKRatio.coupling line 18

    Also declared: ComparatorChallenges/SKRatio.lean:17 (same declaration text).

  6. def OAI.SKRatio.hamiltonian line 22

    Also declared: ComparatorChallenges/SKRatio.lean:21 (same declaration text).

  7. def OAI.SKRatio.weight line 26

    Also declared: ComparatorChallenges/SKRatio.lean:25 (same declaration text).

  8. def OAI.SKRatio.partition line 29

    Also declared: ComparatorChallenges/SKRatio.lean:28 (same declaration text).

  9. def OAI.SKRatio.mass line 32

    Also declared: ComparatorChallenges/SKRatio.lean:31 (same declaration text).

  10. def OAI.SKRatio.flip line 35

    Also declared: ComparatorChallenges/SKRatio.lean:34 (same declaration text).

  11. def OAI.SKRatio.disorderLaw line 38

    Also declared: ComparatorChallenges/SKRatio.lean:37 (same declaration text).

  12. def OAI.SKRatio.siteKernel line 41

    Also declared: ComparatorChallenges/SKRatio.lean:40 (same declaration text).

  13. def OAI.SKRatio.transition line 47

    Also declared: ComparatorChallenges/SKRatio.lean:46 (same declaration text).

  14. def OAI.SKRatio.totalVariation line 50

    Also declared: ComparatorChallenges/SKRatio.lean:49 (same declaration text).

  15. def OAI.SKRatio.discreteDistance line 53

    Also declared: ComparatorChallenges/SKRatio.lean:52 (same declaration text).

  16. def OAI.SKRatio.mixingTime line 57

    Also declared: ComparatorChallenges/SKRatio.lean:56 (same declaration text).

  17. theorem OAI.SKRatio.coupling_diag line 63
  18. theorem OAI.SKRatio.coupling_symm line 66
  19. theorem OAI.SKRatio.flip_same line 72
  20. theorem OAI.SKRatio.flip_other line 75
  21. theorem OAI.SKRatio.flip_flip line 78
  22. theorem OAI.SKRatio.flip_ne line 84
  23. theorem OAI.SKRatio.weight_pos line 89
  24. theorem OAI.SKRatio.partition_pos line 92
  25. theorem OAI.SKRatio.mass_pos line 95
  26. theorem OAI.SKRatio.mass_nonneg line 98
  27. theorem OAI.SKRatio.sum_mass line 101
  28. theorem OAI.SKRatio.mass_le_one line 105
  29. instance OAI.SKRatio.disorderLaw_probability line 112
  30. theorem OAI.SKRatio.siteKernel_nonneg line 121
  31. theorem OAI.SKRatio.sum_siteKernel line 128
  32. theorem OAI.SKRatio.siteKernel_balance line 136
  33. theorem OAI.SKRatio.siteKernel_stationary line 153
  34. theorem OAI.SKRatio.transition_stochastic line 158
  35. theorem OAI.SKRatio.transition_nonneg line 173
  36. theorem OAI.SKRatio.transition_stationary line 176
  37. theorem OAI.SKRatio.transition_pow_stochastic line 186
  38. theorem OAI.SKRatio.transition_pow_stationary line 190
  39. theorem OAI.SKRatio.siteKernel_update_pos line 196
  40. theorem OAI.SKRatio.transition_update_pos line 210
  41. def OAI.SKRatio.updatePath line 218
  42. theorem OAI.SKRatio.updatePath_zero line 221
  43. theorem OAI.SKRatio.updatePath_end line 224
  44. theorem OAI.SKRatio.updatePath_succ line 227
  45. theorem OAI.SKRatio.transition_n_pos line 238
  46. theorem OAI.SKRatio.totalVariation_nonneg line 262
  47. theorem OAI.SKRatio.totalVariation_le_one line 266
  48. theorem OAI.SKRatio.totalVariation_dirac line 278
  49. theorem OAI.SKRatio.totalVariation_minorization line 295
  50. theorem OAI.SKRatio.totalVariation_contract line 329
  51. theorem OAI.SKRatio.exists_geometric_block_bound line 335
  52. theorem OAI.SKRatio.tv_le_discreteDistance line 388