OAI/Probability/IsingPerceptron/GaussianVariance.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Variance.

  1. def OAI.IsingPerceptron.Main.CoordinateLipschitz line 14
  2. lemma OAI.IsingPerceptron.Main.coordinateLipschitz_global line 17
  3. lemma OAI.IsingPerceptron.Main.coordinateLipschitz_memLp line 44
  4. lemma OAI.IsingPerceptron.Main.standardGaussian_second_moment line 63
  5. lemma OAI.IsingPerceptron.Main.gaussian_variance_le_square line 69
  6. lemma OAI.IsingPerceptron.Main.variance_prod_le_of_slices line 90
  7. theorem OAI.IsingPerceptron.Main.gaussian_pi_variance_le line 114
  8. abbrev OAI.IsingPerceptron.Main.Spins line 191
  9. def OAI.IsingPerceptron.Main.spin line 193
  10. def OAI.IsingPerceptron.Main.patternCount line 195
  11. abbrev OAI.IsingPerceptron.Main.Disorder line 197
  12. def OAI.IsingPerceptron.Main.disorderLaw line 199
  13. def OAI.IsingPerceptron.Main.patternEvaluation line 202
  14. def OAI.IsingPerceptron.Main.partitionFunction line 206
  15. def OAI.IsingPerceptron.Main.pressure line 209
  16. def OAI.IsingPerceptron.Main.meanPressure line 212
  17. structure OAI.IsingPerceptron.Main.Partition line 215
  18. structure OAI.IsingPerceptron.Main.StepPath line 223
  19. def OAI.IsingPerceptron.Main.StepPath.stepValue line 228
  20. abbrev OAI.IsingPerceptron.Main.StepField line 232
  21. abbrev OAI.IsingPerceptron.Main.StepOverlap line 233
  22. def OAI.IsingPerceptron.Main.gaussianTransform line 235
  23. def OAI.IsingPerceptron.Main.StepPath.increment line 239
  24. def OAI.IsingPerceptron.Main.stepPattern line 244
  25. def OAI.IsingPerceptron.Main.fieldFunctional line 248
  26. abbrev OAI.IsingPerceptron.Main.OpenUnit line 254
  27. abbrev OAI.IsingPerceptron.Main.OverlapRep line 255
  28. def OAI.IsingPerceptron.Main.extendRep line 257
  29. def OAI.IsingPerceptron.Main.pathSetoid line 260
  30. def OAI.IsingPerceptron.Main.OverlapPath line 265
  31. def OAI.IsingPerceptron.Main.uniformPartition line 267
  32. def OAI.IsingPerceptron.Main.midpoint line 277
  33. lemma OAI.IsingPerceptron.Main.midpoint_monotone line 287
  34. def OAI.IsingPerceptron.Main.dyadicStep line 294
  35. def OAI.IsingPerceptron.Main.patternFunctional line 302
  36. def OAI.IsingPerceptron.Main.isingEntropy line 305
  37. def OAI.IsingPerceptron.Main.variationalValue line 310
  38. def OAI.IsingPerceptron.Main.PressureConvergesInProbability line 313
  39. lemma OAI.IsingPerceptron.Main.spin_card line 324
  40. lemma OAI.IsingPerceptron.Main.finite_exp_average_pos line 326
  41. lemma OAI.IsingPerceptron.Main.finite_log_average_le line 332
  42. lemma OAI.IsingPerceptron.Main.finite_log_average_abs line 348
  43. lemma OAI.IsingPerceptron.Main.finite_log_average_difference line 357
  44. lemma OAI.IsingPerceptron.Main.pressure_measurable line 365
  45. lemma OAI.IsingPerceptron.Main.pressure_bounded line 370
  46. lemma OAI.IsingPerceptron.Main.pressure_row_difference line 382
  47. theorem OAI.IsingPerceptron.Main.pressure_variance_bound line 405
  48. lemma OAI.IsingPerceptron.Main.pressure_variance_rate line 415
  49. theorem OAI.IsingPerceptron.Main.pressure_tail_bound line 424
  50. theorem OAI.IsingPerceptron.Main.pressure_centered_concentration line 442
  51. def OAI.IsingPerceptron.Main.finiteGibbs line 462
  52. lemma OAI.IsingPerceptron.Main.finiteGibbs_den_pos line 464
  53. lemma OAI.IsingPerceptron.Main.finiteGibbs_abs line 467
  54. lemma OAI.IsingPerceptron.Main.finiteGibbs_add line 477
  55. lemma OAI.IsingPerceptron.Main.finiteGibbs_mul_const line 482
  56. lemma OAI.IsingPerceptron.Main.finiteGibbs_div_const line 488
  57. lemma OAI.IsingPerceptron.Main.finiteGibbs_measurable line 493
  58. theorem OAI.IsingPerceptron.Main.finiteGibbs_derivative line 500
  59. lemma OAI.IsingPerceptron.Main.finiteGibbs_sum line 518
  60. lemma OAI.IsingPerceptron.Main.finiteGibbs_const_mul line 524
  61. def OAI.IsingPerceptron.Main.finiteGibbsPair line 528
  62. lemma OAI.IsingPerceptron.Main.standardDensity_derivative line 537
  63. lemma OAI.IsingPerceptron.Main.standardDensity_times_id_integrable line 550
  64. theorem OAI.IsingPerceptron.Main.gaussian_integration_by_parts line 559
  65. theorem OAI.IsingPerceptron.Main.gaussian_pi_integration_by_parts line 583