OAI/Probability/IsingPerceptron/GaussianGibbs.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Gibbs.

  1. lemma OAI.IsingPerceptron.Main.finiteFunction_bound line 16
  2. lemma OAI.IsingPerceptron.Main.finiteGibbs_const line 19
  3. lemma OAI.IsingPerceptron.Main.finiteGibbs_sub line 23
  4. def OAI.IsingPerceptron.Main.gaussianLinear line 27
  5. def OAI.IsingPerceptron.Main.gaussianGibbsH line 30
  6. lemma OAI.IsingPerceptron.Main.gaussianLinear_derivative line 34
  7. lemma OAI.IsingPerceptron.Main.gaussianGibbs_measurable line 48
  8. lemma OAI.IsingPerceptron.Main.gaussianGibbs_integrable line 55
  9. lemma OAI.IsingPerceptron.Main.gaussianGibbs_derivative line 62
  10. lemma OAI.IsingPerceptron.Main.gaussianGibbs_coordinate_ibp line 78
  11. theorem OAI.IsingPerceptron.Main.gaussianGibbs_ibp line 109
  12. def OAI.IsingPerceptron.Main.replicasEnergy line 162
  13. def OAI.IsingPerceptron.Main.replicatedGibbs line 164
  14. lemma OAI.IsingPerceptron.Main.replicatedGibbs_product line 168
  15. lemma OAI.IsingPerceptron.Main.replicatedGibbs_marginal line 175
  16. def OAI.IsingPerceptron.Main.gaussianCoefficientCov line 183
  17. lemma OAI.IsingPerceptron.Main.replicas_gaussian_hamiltonian line 187
  18. theorem OAI.IsingPerceptron.Main.replicated_gaussian_ibp line 199
  19. instance OAI.IsingPerceptron.Main.mvGaussian_probability line 245
  20. theorem OAI.IsingPerceptron.Main.multivariateGaussian_tendsto line 250
  21. theorem OAI.IsingPerceptron.Main.gaussian_test_tendsto line 270
  22. abbrev OAI.IsingPerceptron.Main.CovarianceMatrix line 280
  23. lemma OAI.IsingPerceptron.Main.probability_dirac_tendsto line 282
  24. theorem OAI.IsingPerceptron.Main.gaussian_mixed_test_continuous line 290
  25. theorem OAI.IsingPerceptron.Main.gaussian_mixed_test_limit line 314
  26. theorem OAI.IsingPerceptron.Main.gaussian_matrix_image line 344
  27. def OAI.IsingPerceptron.Main.freshRowLaw line 371
  28. instance OAI.IsingPerceptron.Main.freshRowLaw_probability line 373
  29. def OAI.IsingPerceptron.Main.spinOverlap line 376
  30. def OAI.IsingPerceptron.Main.freshPatternVector line 378
  31. theorem OAI.IsingPerceptron.Main.freshPattern_law line 381
  32. def OAI.IsingPerceptron.Main.tensorEnumeration line 416
  33. def OAI.IsingPerceptron.Main.tensorCoefficient line 422
  34. def OAI.IsingPerceptron.Main.tensorPerturbation line 426
  35. lemma OAI.IsingPerceptron.Main.tensor_covariance line 430
  36. theorem OAI.IsingPerceptron.Main.actual_tensor_replica_ibp line 443
  37. def OAI.IsingPerceptron.Main.finiteLogPartition line 460
  38. def OAI.IsingPerceptron.Main.linearLogPartition line 463
  39. lemma OAI.IsingPerceptron.Main.linearLogPartition_measurable line 467
  40. lemma OAI.IsingPerceptron.Main.linearLogPartition_coordinate line 472
  41. lemma OAI.IsingPerceptron.Main.linearLogPartition_memLp line 487
  42. theorem OAI.IsingPerceptron.Main.linearLogPartition_variance line 494
  43. lemma OAI.IsingPerceptron.Main.tensorCoefficient_abs line 501
  44. lemma OAI.IsingPerceptron.Main.tensor_coordinate_squares line 511
  45. theorem OAI.IsingPerceptron.Main.tensor_logPartition_variance line 521