OAI/Probability/IsingPerceptron/LabeledSampling.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Labeled Sampling.

  1. lemma OAI.IsingPerceptron.measurable_lintegral_pointwiseFinite line 15
  2. def OAI.IsingPerceptron.finitePartKernel line 51
  3. lemma OAI.IsingPerceptron.finitePartKernel_finite line 57
  4. lemma OAI.IsingPerceptron.measurable_finitePart_lintegral line 67
  5. lemma OAI.IsingPerceptron.infinitePi_indep_eval_rest line 73
  6. lemma OAI.IsingPerceptron.infinitePi_eval_rest_map line 89
  7. lemma OAI.IsingPerceptron.measureSum_eq_eval_add_rest line 102
  8. def OAI.IsingPerceptron.atomCloud line 117
  9. lemma OAI.IsingPerceptron.measurable_atomCloud line 120
  10. lemma OAI.IsingPerceptron.atomCloud_insertNth line 124
  11. lemma OAI.IsingPerceptron.atomCloud_lintegral line 131
  12. lemma OAI.IsingPerceptron.iid_point_insertion line 135
  13. lemma OAI.IsingPerceptron.iid_sum_point_insertion line 158
  14. def OAI.IsingPerceptron.poissonWeight line 168
  15. lemma OAI.IsingPerceptron.poissonWeight_succ line 171
  16. lemma OAI.IsingPerceptron.iid_restrict_lintegral line 186
  17. lemma OAI.IsingPerceptron.lintegral_finitePoissonCloud line 196
  18. theorem OAI.IsingPerceptron.finitePoissonCloud_insertion line 213
  19. lemma OAI.IsingPerceptron.measurable_measureSum_countable line 252
  20. lemma OAI.IsingPerceptron.measurable_finitePart_param line 259
  21. lemma OAI.IsingPerceptron.finitePoissonLaw_finite line 270
  22. lemma OAI.IsingPerceptron.finitePoissonLaw_insertion line 280
  23. lemma OAI.IsingPerceptron.poissonComponent_insertion line 293
  24. lemma OAI.IsingPerceptron.poissonProductLaw_finite line 347
  25. theorem OAI.IsingPerceptron.poissonProductLaw_insertion line 360
  26. lemma OAI.IsingPerceptron.poissonProductLaw_mean_count line 381
  27. lemma OAI.IsingPerceptron.poissonLaw_mean_count line 390
  28. lemma OAI.IsingPerceptron.measurable_measureRestrict line 397
  29. def OAI.IsingPerceptron.sigmaPart line 406
  30. lemma OAI.IsingPerceptron.sigmaPart_eq_ae line 409
  31. lemma OAI.IsingPerceptron.measurable_sigmaPart_param line 430
  32. lemma OAI.IsingPerceptron.poissonLaw_campbell_aemeasurable line 440
  33. theorem OAI.IsingPerceptron.poissonLaw_insertion line 450
  34. def OAI.IsingPerceptron.PoissonGood line 467
  35. lemma OAI.IsingPerceptron.poissonGood_ae line 470
  36. lemma OAI.IsingPerceptron.sigmaPart_eq_of_good line 480
  37. lemma OAI.IsingPerceptron.PoissonGood.dirac_add line 491
  38. def OAI.IsingPerceptron.poissonFactorial line 499
  39. lemma OAI.IsingPerceptron.measurable_fin_cons_param line 507
  40. lemma OAI.IsingPerceptron.measurable_poissonFactorial_param line 516
  41. lemma OAI.IsingPerceptron.poissonFactorial_dirac_add line 539
  42. def OAI.IsingPerceptron.poissonLaplaceWeight line 576
  43. lemma OAI.IsingPerceptron.measurable_poissonLaplaceWeight line 579
  44. lemma OAI.IsingPerceptron.poissonLaplaceWeight_dirac_add line 583
  45. lemma OAI.IsingPerceptron.measurable_poissonFactorial_body line 589
  46. lemma OAI.IsingPerceptron.poissonFactorial_laplace_step line 603
  47. theorem OAI.IsingPerceptron.poissonFactorial_laplace line 642