OAI/Probability/IsingPerceptron/GaussianIntegration.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Integration.

  1. lemma OAI.IsingPerceptron.hasDerivAt_standardGaussianPDF line 13
  2. lemma OAI.IsingPerceptron.integrable_gaussian_iff line 23
  3. lemma OAI.IsingPerceptron.gaussian_integration_by_parts line 32
  4. lemma OAI.IsingPerceptron.gaussian_integration_by_parts_bounded line 57
  5. lemma OAI.IsingPerceptron.gaussian_pi_integration_by_parts line 73
  6. def OAI.IsingPerceptron.finitePartition line 116
  7. def OAI.IsingPerceptron.finiteGibbs line 117
  8. def OAI.IsingPerceptron.GibbsReference line 120
  9. lemma OAI.IsingPerceptron.finitePartition_pos line 122
  10. lemma OAI.IsingPerceptron.finiteGibbs_nonneg line 128
  11. lemma OAI.IsingPerceptron.finiteGibbs_sum line 132
  12. lemma OAI.IsingPerceptron.finiteGibbs_le_one line 137
  13. lemma OAI.IsingPerceptron.finiteGibbs_average_bound line 142
  14. lemma OAI.IsingPerceptron.hasDerivAt_finitePartition line 153
  15. lemma OAI.IsingPerceptron.hasDerivAt_finiteGibbs line 160
  16. lemma OAI.IsingPerceptron.hasDerivAt_log_finitePartition line 172
  17. def OAI.IsingPerceptron.linearGaussian line 185
  18. def OAI.IsingPerceptron.gaussianGibbs line 188
  19. lemma OAI.IsingPerceptron.continuous_gaussianGibbs line 192
  20. lemma OAI.IsingPerceptron.hasDerivAt_linearGaussian_insert line 202
  21. lemma OAI.IsingPerceptron.hasDerivAt_gaussianGibbs_insert line 214
  22. lemma OAI.IsingPerceptron.gaussian_gibbs_coordinate_insertion line 224
  23. def OAI.IsingPerceptron.replicaGibbs line 260
  24. lemma OAI.IsingPerceptron.replicaGibbs_nonneg line 264
  25. lemma OAI.IsingPerceptron.replicaGibbs_le_one line 269
  26. lemma OAI.IsingPerceptron.replicaGibbs_sum line 275
  27. lemma OAI.IsingPerceptron.continuous_replicaGibbs line 283
  28. lemma OAI.IsingPerceptron.hasDerivAt_replicaGibbs_insert line 288
  29. lemma OAI.IsingPerceptron.gaussian_replica_coordinate_insertion line 303
  30. lemma OAI.IsingPerceptron.integrable_gaussian_coordinate_mul line 337
  31. lemma OAI.IsingPerceptron.gaussian_pi_linear_insertion line 347
  32. def OAI.IsingPerceptron.gaussianCross line 367
  33. lemma OAI.IsingPerceptron.gaussian_replica_insertion line 370
  34. lemma OAI.IsingPerceptron.log_finitePartition_le_add line 425
  35. lemma OAI.IsingPerceptron.log_finitePartition_lipschitz line 437
  36. lemma OAI.IsingPerceptron.integrable_linearGaussian line 450
  37. lemma OAI.IsingPerceptron.continuous_log_finitePartition line 458
  38. lemma OAI.IsingPerceptron.integrable_log_finitePartition line 465
  39. lemma OAI.IsingPerceptron.hasDerivAt_expected_log_finitePartition line 488
  40. lemma OAI.IsingPerceptron.linearGaussian_scale line 524
  41. lemma OAI.IsingPerceptron.gaussianCross_scale line 529
  42. lemma OAI.IsingPerceptron.gaussian_gibbs_insertion line 536
  43. lemma OAI.IsingPerceptron.integrable_linearGaussian_mul_gibbs line 546
  44. lemma OAI.IsingPerceptron.hasDerivAt_expected_log_gaussian line 557
  45. lemma OAI.IsingPerceptron.gaussian_covariance_difference_bound line 577
  46. lemma OAI.IsingPerceptron.integrable_gaussian_covariance_insertion line 591
  47. def OAI.IsingPerceptron.expectedGaussianLog line 610
  48. def OAI.IsingPerceptron.gaussianLogDerivative line 614
  49. lemma OAI.IsingPerceptron.gaussianLogDerivative_bound line 621
  50. theorem OAI.IsingPerceptron.gaussian_perturbation_cost line 638
  51. lemma OAI.IsingPerceptron.hasDerivAt_finiteGibbs_mean line 680
  52. lemma OAI.IsingPerceptron.convexOn_log_finitePartition line 701
  53. abbrev OAI.IsingPerceptron.Spin line 716
  54. abbrev OAI.IsingPerceptron.Patterns line 717
  55. def OAI.IsingPerceptron.spinValue line 719
  56. def OAI.IsingPerceptron.patternCount line 721
  57. def OAI.IsingPerceptron.projection line 723
  58. def OAI.IsingPerceptron.partitionFunction line 726
  59. def OAI.IsingPerceptron.pressure line 731
  60. def OAI.IsingPerceptron.gaussianPatterns line 735
  61. def OAI.IsingPerceptron.spinOverlap line 738
  62. def OAI.IsingPerceptron.spinTensor line 741
  63. lemma OAI.IsingPerceptron.abs_spinValue line 744
  64. lemma OAI.IsingPerceptron.spinOverlap_diag line 748
  65. lemma OAI.IsingPerceptron.abs_spinOverlap_le line 754
  66. lemma OAI.IsingPerceptron.spinTensor_covariance line 762
  67. abbrev OAI.IsingPerceptron.BulkCoordinate line 772
  68. def OAI.IsingPerceptron.bulkCoefficient line 774
  69. def OAI.IsingPerceptron.bulkCovariance line 777
  70. lemma OAI.IsingPerceptron.bulkCoefficient_covariance line 780
  71. lemma OAI.IsingPerceptron.bulkCovariance_abs_le line 793
  72. def OAI.IsingPerceptron.indexedBulkCoefficient line 821
  73. lemma OAI.IsingPerceptron.indexedBulkCoefficient_covariance line 825
  74. lemma OAI.IsingPerceptron.bulk_gaussian_perturbation_cost line 835
  75. lemma OAI.IsingPerceptron.coordinatewise_lipschitz_sum line 845
  76. lemma OAI.IsingPerceptron.memLp_gaussian_coordinatewise line 875
  77. lemma OAI.IsingPerceptron.memLp_gaussian_lipschitz line 897
  78. lemma OAI.IsingPerceptron.variance_gaussian_lipschitz line 911
  79. lemma OAI.IsingPerceptron.variance_prod_section_bound line 933
  80. lemma OAI.IsingPerceptron.variance_gaussian_coordinatewise line 956
  81. lemma OAI.IsingPerceptron.log_finitePartition_coordinate_lipschitz line 1021
  82. lemma OAI.IsingPerceptron.variance_gaussian_log_finitePartition line 1046
  83. lemma OAI.IsingPerceptron.abs_spinTensor_independent line 1061
  84. lemma OAI.IsingPerceptron.abs_bulkCoefficient_independent line 1066
  85. lemma OAI.IsingPerceptron.abs_indexedBulkCoefficient_independent line 1071
  86. lemma OAI.IsingPerceptron.bulk_gaussian_variance line 1077
  87. def OAI.IsingPerceptron.replicaMean line 1102
  88. def OAI.IsingPerceptron.expectedReplica line 1106
  89. lemma OAI.IsingPerceptron.replicaMean_abs_le line 1110
  90. lemma OAI.IsingPerceptron.integrable_replicaMean line 1126
  91. lemma OAI.IsingPerceptron.integrable_linear_mul_replica line 1137
  92. lemma OAI.IsingPerceptron.integrable_replica_covariance line 1148
  93. lemma OAI.IsingPerceptron.gaussian_replica_test_insertion line 1177
  94. lemma OAI.IsingPerceptron.replicaMean_marginal_zero line 1192