OAI/MathematicalPhysics/CriticalSK/HeatBath.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.gibbs_sqrt_pos line 39
  2. def OAI.CriticalSK.gibbsEuclideanEquiv line 42
  3. lemma OAI.CriticalSK.gibbsEuclideanEquiv_apply line 55
  4. lemma OAI.CriticalSK.gibbsEuclideanEquiv_symm_apply line 58
  5. lemma OAI.CriticalSK.gibbsEuclideanEquiv_inner line 61
  6. def OAI.CriticalSK.kernelConjugate line 73
  7. lemma OAI.CriticalSK.kernelConjugate_apply line 76
  8. lemma OAI.CriticalSK.kernelConjugate_isHermitian line 87
  9. lemma OAI.CriticalSK.discreteKernel_nonneg line 98
  10. lemma OAI.CriticalSK.discreteKernel_sum line 104
  11. lemma OAI.CriticalSK.discreteKernel_reversible line 111
  12. lemma OAI.CriticalSK.discreteKernel_stationary line 126
  13. lemma OAI.CriticalSK.discreteKernel_average line 131
  14. lemma OAI.CriticalSK.siteAverage_self_square line 136
  15. lemma OAI.CriticalSK.discreteKernel_quadratic_nonneg line 142
  16. lemma OAI.CriticalSK.generator_discreteKernel line 152
  17. lemma OAI.CriticalSK.dirichlet_discrete line 158
  18. lemma OAI.CriticalSK.hermitian_eigenbasis_apply line 180
  19. lemma OAI.CriticalSK.hermitian_repr_apply line 186
  20. lemma OAI.CriticalSK.hermitian_repr_pow line 193
  21. lemma OAI.CriticalSK.hermitian_inner_sub_pow line 204
  22. lemma OAI.CriticalSK.one_sub_pow_le_mul line 214
  23. lemma OAI.CriticalSK.hermitian_power_increment_le line 224
  24. lemma OAI.CriticalSK.kernelConjugate_pow_apply line 245
  25. lemma OAI.CriticalSK.discreteKernel_eigenvalues line 257
  26. theorem OAI.CriticalSK.discrete_inner_increment_le line 281
  27. lemma OAI.CriticalSK.kernel_mul_nonneg line 302
  28. lemma OAI.CriticalSK.kernel_mul_sum line 308
  29. lemma OAI.CriticalSK.kernel_mul_stationary line 317
  30. lemma OAI.CriticalSK.kernel_pow_nonneg line 326
  31. lemma OAI.CriticalSK.kernel_pow_sum line 332
  32. lemma OAI.CriticalSK.kernel_pow_stationary line 338
  33. lemma OAI.CriticalSK.stationary_increment_identity line 346
  34. theorem OAI.CriticalSK.stationary_increment_discrete line 387
  35. lemma OAI.CriticalSK.matrix_exp_hasSum line 406
  36. lemma OAI.CriticalSK.matrix_exp_entry_hasSum line 410
  37. lemma OAI.CriticalSK.matrix_exp_scalar line 414
  38. lemma OAI.CriticalSK.matrix_poisson_exp line 420
  39. lemma OAI.CriticalSK.matrix_poisson_hasSum line 429
  40. lemma OAI.CriticalSK.poisson_coeff_hasSum line 440
  41. lemma OAI.CriticalSK.poisson_coeff_moment_hasSum line 449
  42. lemma OAI.CriticalSK.poisson_coeff_nonneg line 462
  43. lemma OAI.CriticalSK.poisson_kernel_nonneg line 471
  44. lemma OAI.CriticalSK.poisson_kernel_sum line 478
  45. lemma OAI.CriticalSK.poisson_kernel_stationary line 484
  46. lemma OAI.CriticalSK.poisson_stationary_increment_le line 494
  47. lemma OAI.CriticalSK.continuousKernel_poisson line 527
  48. lemma OAI.CriticalSK.continuousKernel_nonneg line 531
  49. lemma OAI.CriticalSK.continuousKernel_sum line 537
  50. lemma OAI.CriticalSK.continuousKernel_stationary line 542
  51. theorem OAI.CriticalSK.stationary_increment_continuous line 547
  52. lemma OAI.CriticalSK.finite_event_test line 571
  53. lemma OAI.CriticalSK.odd_halfspace_mass_le line 598
  54. lemma OAI.CriticalSK.sign_row_test line 620
  55. lemma OAI.CriticalSK.sign_failure_pointwise line 634
  56. lemma OAI.CriticalSK.sign_failure_average line 649
  57. lemma OAI.CriticalSK.good_mass_complement line 681
  58. lemma OAI.CriticalSK.sign_good_mass_bound line 691
  59. theorem OAI.CriticalSK.continuous_good_mass_bound line 721
  60. theorem OAI.CriticalSK.discrete_good_mass_bound line 737