OAI/Probability/SKRatio/FiniteChain/Mean.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.FiniteLaw.mean line 17
  2. def OAI.SKRatio.FiniteLaw.variance line 19
  3. theorem OAI.SKRatio.FiniteLaw.variance_eq line 22
  4. theorem OAI.SKRatio.FiniteLaw.common_mass line 31
  5. theorem OAI.SKRatio.FiniteLaw.common_mass_square line 41
  6. theorem OAI.SKRatio.FiniteLaw.totalVariation_square line 59
  7. theorem OAI.SKRatio.Independent.spinValue_sq line 72
  8. theorem OAI.SKRatio.Independent.spinValue_not line 75
  9. theorem OAI.SKRatio.Independent.coupling_zero line 78
  10. theorem OAI.SKRatio.Independent.mass_zero line 81
  11. theorem OAI.SKRatio.Independent.siteKernel_zero line 84
  12. def OAI.SKRatio.Independent.character line 92
  13. theorem OAI.SKRatio.Independent.character_empty line 94
  14. theorem OAI.SKRatio.Independent.character_sq line 96
  15. theorem OAI.SKRatio.Independent.character_plus line 99
  16. theorem OAI.SKRatio.Independent.character_flip line 102
  17. theorem OAI.SKRatio.Independent.character_complete line 117
  18. def OAI.SKRatio.Independent.eigenvalue line 134
  19. theorem OAI.SKRatio.Independent.siteKernel_character line 136
  20. theorem OAI.SKRatio.Independent.transition_character line 143
  21. theorem OAI.SKRatio.Independent.power_character line 159
  22. theorem OAI.SKRatio.Independent.return_probability line 179
  23. theorem OAI.SKRatio.Independent.transition_isSymm line 196
  24. theorem OAI.SKRatio.Independent.eigenvalue_nonneg line 211
  25. theorem OAI.SKRatio.Independent.eigenvalue_exp_bound line 216
  26. theorem OAI.SKRatio.Independent.sum_eigenvalue_bound line 226
  27. theorem OAI.SKRatio.Independent.row_square line 239
  28. theorem OAI.SKRatio.Independent.row_centered_square line 251
  29. theorem OAI.SKRatio.Independent.row_tv_square_upper line 265
  30. theorem OAI.SKRatio.Independent.distance_upper line 273
  31. def OAI.SKRatio.Independent.flipEquiv line 282
  32. theorem OAI.SKRatio.Independent.mean_character line 288
  33. theorem OAI.SKRatio.Independent.character_singleton line 297
  34. theorem OAI.SKRatio.Independent.character_pair line 300
  35. def OAI.SKRatio.Independent.magnetization line 304
  36. theorem OAI.SKRatio.Independent.row_mean_spin line 306
  37. theorem OAI.SKRatio.Independent.row_mean_pair line 311
  38. theorem OAI.SKRatio.Independent.equilibrium_mean_spin line 317
  39. theorem OAI.SKRatio.Independent.equilibrium_mean_pair line 321
  40. theorem OAI.SKRatio.Independent.row_mean_magnetization line 326
  41. theorem OAI.SKRatio.Independent.equilibrium_mean_magnetization line 336
  42. theorem OAI.SKRatio.Independent.eigenvalue_two_le_square line 344
  43. theorem OAI.SKRatio.Independent.row_variance_magnetization line 355
  44. theorem OAI.SKRatio.Independent.equilibrium_variance_magnetization line 397