OAI/MathematicalPhysics/CriticalSK/GapMixing.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.mean_square_center_identity line 22
  2. lemma OAI.CriticalSK.mean_least_squares line 35
  3. lemma OAI.CriticalSK.mean_density_upper line 40
  4. lemma OAI.CriticalSK.variance_density_upper line 48
  5. lemma OAI.CriticalSK.dirichlet_density_lower line 52
  6. lemma OAI.CriticalSK.poincare_density_comparison line 67
  7. lemma OAI.CriticalSK.hamiltonian_scale line 80
  8. lemma OAI.CriticalSK.gibbs_scale_ratio line 86
  9. lemma OAI.CriticalSK.poincare_temperature_comparison line 96
  10. lemma OAI.CriticalSK.mean_kernel line 134
  11. lemma OAI.CriticalSK.discreteKernel_quadratic_eq line 143
  12. lemma OAI.CriticalSK.discreteKernel_square_le line 148
  13. lemma OAI.CriticalSK.gap_factor_nonneg line 170
  14. lemma OAI.CriticalSK.gap_square_step line 176
  15. lemma OAI.CriticalSK.gap_square_pow line 192
  16. lemma OAI.CriticalSK.gap_square_exponential line 207
  17. lemma OAI.CriticalSK.kernel_pow_reversible line 231
  18. lemma OAI.CriticalSK.mean_abs_square_le line 246
  19. def OAI.CriticalSK.centeredPointDensity line 257
  20. lemma OAI.CriticalSK.centeredPointDensity_mean line 259
  21. lemma OAI.CriticalSK.centeredPointDensity_square line 266
  22. lemma OAI.CriticalSK.centeredPointDensity_kernel line 277
  23. lemma OAI.CriticalSK.discreteDistance_mean_density line 289
  24. lemma OAI.CriticalSK.discreteDistance_square_gap line 305
  25. lemma OAI.CriticalSK.discreteDistance_gap_bound line 318
  26. lemma OAI.CriticalSK.poisson_generating_hasSum line 344
  27. lemma OAI.CriticalSK.finite_l1_series_bound line 353
  28. lemma OAI.CriticalSK.poisson_l1_bound line 371
  29. lemma OAI.CriticalSK.exp_neg_linear_bound line 394
  30. lemma OAI.CriticalSK.continuousDistance_gap_bound line 404
  31. lemma OAI.CriticalSK.exp_neg_two_le_half line 444
  32. lemma OAI.CriticalSK.gibbs_lower_of_energy_bound line 451
  33. lemma OAI.CriticalSK.continuousMixingTime_le_of_distance line 471
  34. lemma OAI.CriticalSK.discreteMixingTime_le_of_distance line 476
  35. lemma OAI.CriticalSK.finite_continuous_gap_mixing line 479
  36. lemma OAI.CriticalSK.finite_discrete_gap_mixing line 495
  37. lemma OAI.CriticalSK.finite_gap_mixing_bounds line 510