OAI/Probability/SKBarriers/Gaussian/SmoothFamily.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. class OAI.SK.Analytic.SmoothFamily.Model line 14
  2. def OAI.SK.Analytic.SmoothFamily.logPartition line 26
  3. def OAI.SK.Analytic.SmoothFamily.gibbs line 27
  4. theorem OAI.SK.Analytic.SmoothFamily.gibbs_nonneg line 29
  5. theorem OAI.SK.Analytic.SmoothFamily.gibbs_sum line 32
  6. theorem OAI.SK.Analytic.SmoothFamily.continuous_gibbs line 35
  7. theorem OAI.SK.Analytic.SmoothFamily.continuous_logPartition line 38
  8. def OAI.SK.Analytic.SmoothFamily.directionalEnergy line 40
  9. theorem OAI.SK.Analytic.SmoothFamily.directionalEnergy_exp_le line 43
  10. theorem OAI.SK.Analytic.SmoothFamily.gibbs_le_one line 53
  11. theorem OAI.SK.Analytic.SmoothFamily.gibbs_integrable line 58
  12. theorem OAI.SK.Analytic.SmoothFamily.continuous_directionalEnergy line 64
  13. theorem OAI.SK.Analytic.SmoothFamily.directionalEnergy_exp_integrable line 71
  14. theorem OAI.SK.Analytic.SmoothFamily.directionalEnergy_exp_integral_le line 86
  15. theorem OAI.SK.Analytic.SmoothFamily.directionalEnergy_pair_exp_integrable line 103
  16. theorem OAI.SK.Analytic.SmoothFamily.directionalEnergy_pair_exp_integral_le line 120
  17. theorem OAI.SK.Analytic.SmoothFamily.logPartition_hasDerivAt line 132
  18. theorem OAI.SK.Analytic.SmoothFamily.rotation_logPartition_hasDerivAt line 138
  19. theorem OAI.SK.Analytic.SmoothFamily.continuous_rotation_energy line 154
  20. theorem OAI.SK.Analytic.SmoothFamily.rotation_logPartition_integral line 159
  21. theorem OAI.SK.Analytic.SmoothFamily.rotation_exp_jensen line 174
  22. theorem OAI.SK.Analytic.SmoothFamily.rotated_directionalEnergy_exp_integrable line 193
  23. theorem OAI.SK.Analytic.SmoothFamily.rotated_directionalEnergy_exp_integral_le line 200
  24. def OAI.SK.Analytic.SmoothFamily.rotationIntegrand line 216
  25. theorem OAI.SK.Analytic.SmoothFamily.continuous_rotationIntegrand line 220
  26. theorem OAI.SK.Analytic.SmoothFamily.rotationIntegrand_integrable line 235
  27. theorem OAI.SK.Analytic.SmoothFamily.rotation_exp_integrable line 254
  28. theorem OAI.SK.Analytic.SmoothFamily.rotation_exp_integral_le line 272
  29. theorem OAI.SK.Analytic.SmoothFamily.rotateDisorder_pi_div_two_fst line 307
  30. theorem OAI.SK.Analytic.SmoothFamily.logPartition_difference_exp_integrable line 312
  31. theorem OAI.SK.Analytic.SmoothFamily.logPartition_exp_integrable line 318
  32. theorem OAI.SK.Analytic.SmoothFamily.logPartition_integrable line 329
  33. theorem OAI.SK.Analytic.SmoothFamily.logPartition_centered_exp_jensen line 346
  34. theorem OAI.SK.Analytic.SmoothFamily.logPartition_centered_exp_integrable line 367
  35. theorem OAI.SK.Analytic.SmoothFamily.logPartition_centered_exp_integral_le line 379
  36. theorem OAI.SK.Analytic.SmoothFamily.logPartition_subGaussian line 406
  37. theorem OAI.SK.Analytic.SmoothFamily.logPartition_upper_tail line 418
  38. theorem OAI.SK.Analytic.SmoothFamily.logPartition_lower_tail line 423