OAI/Probability/IsingPerceptron/PoissonCloud.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Poisson Cloud.

  1. lemma OAI.IsingPerceptron.poisson_probability_generating line 23
  2. def OAI.IsingPerceptron.finitePoissonCloud line 42
  3. instance OAI.IsingPerceptron.finitePoissonCloud_probability line 45
  4. def OAI.IsingPerceptron.cloudSum line 50
  5. lemma OAI.IsingPerceptron.measurable_cloudSum line 53
  6. lemma OAI.IsingPerceptron.iid_finite_laplace line 61
  7. theorem OAI.IsingPerceptron.finitePoissonCloud_laplace line 83
  8. lemma OAI.IsingPerceptron.poisson_complex_generating line 98
  9. lemma OAI.IsingPerceptron.iid_finite_fourier line 116
  10. theorem OAI.IsingPerceptron.finitePoissonCloud_fourier line 139
  11. def OAI.IsingPerceptron.enegExp line 152
  12. def OAI.IsingPerceptron.negExp line 153
  13. lemma OAI.IsingPerceptron.enegExp_le_one line 155
  14. lemma OAI.IsingPerceptron.enegExp_ne_top line 157
  15. lemma OAI.IsingPerceptron.continuous_enegExp line 159
  16. lemma OAI.IsingPerceptron.continuous_negExp line 161
  17. lemma OAI.IsingPerceptron.negExp_nonneg line 164
  18. lemma OAI.IsingPerceptron.negExp_le_one line 165
  19. lemma OAI.IsingPerceptron.negExp_injective line 168
  20. lemma OAI.IsingPerceptron.enegExp_zero line 174
  21. lemma OAI.IsingPerceptron.enegExp_top line 175
  22. lemma OAI.IsingPerceptron.negExp_zero line 176
  23. lemma OAI.IsingPerceptron.negExp_top line 177
  24. lemma OAI.IsingPerceptron.negExp_ofReal line 178
  25. lemma OAI.IsingPerceptron.enegExp_add line 182
  26. lemma OAI.IsingPerceptron.negExp_add line 194
  27. lemma OAI.IsingPerceptron.negExp_sum line 196
  28. lemma OAI.IsingPerceptron.negExp_nat_mul line 202
  29. def OAI.IsingPerceptron.finiteCloudMeasure line 208
  30. lemma OAI.IsingPerceptron.measurable_finiteCloudMeasure line 211
  31. lemma OAI.IsingPerceptron.finiteCloudMeasure_lintegral line 218
  32. def OAI.IsingPerceptron.finitePoissonLaw line 225
  33. instance OAI.IsingPerceptron.finitePoissonLaw_probability line 228
  34. lemma OAI.IsingPerceptron.finiteMeasure_mass_normalize line 233
  35. lemma OAI.IsingPerceptron.finitePoissonLaw_laplace line 239
  36. def OAI.IsingPerceptron.poissonComponentLaw line 276
  37. instance OAI.IsingPerceptron.poissonComponentLaw_probability line 279
  38. def OAI.IsingPerceptron.poissonProductLaw line 283
  39. instance OAI.IsingPerceptron.poissonProductLaw_probability line 286
  40. lemma OAI.IsingPerceptron.measurable_measureSum line 290
  41. def OAI.IsingPerceptron.poissonLaw line 297
  42. instance OAI.IsingPerceptron.poissonLaw_probability line 300
  43. lemma OAI.IsingPerceptron.laplace_partial_tendsto line 305
  44. lemma OAI.IsingPerceptron.poissonProductLaw_laplace_partial line 324
  45. theorem OAI.IsingPerceptron.poissonLaw_laplace line 348
  46. def OAI.IsingPerceptron.negExpBCF line 372
  47. lemma OAI.IsingPerceptron.laplace_finite_coordinates_unique line 376
  48. lemma OAI.IsingPerceptron.measure_eq_of_map_eq_comap line 421
  49. def OAI.IsingPerceptron.measureCoordinates line 431
  50. lemma OAI.IsingPerceptron.measurable_measureCoordinates line 434
  51. lemma OAI.IsingPerceptron.measureSpace_eq_comap_coordinates line 438
  52. theorem OAI.IsingPerceptron.randomMeasure_laplace_unique line 457
  53. theorem OAI.IsingPerceptron.poissonLaw_map line 514