OAI/Probability/IsingPerceptron/LintegralGammaKernel.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Lintegral Gamma Kernel.

  1. lemma OAI.IsingPerceptron.lintegral_gamma_kernel line 15
  2. lemma OAI.IsingPerceptron.inverse_power_laplace line 29
  3. lemma OAI.IsingPerceptron.expected_inverse_power line 41
  4. instance OAI.IsingPerceptron.powerIntensity_nullSingleton line 80
  5. lemma OAI.IsingPerceptron.powerIntensity_moment_laplace line 84
  6. lemma OAI.IsingPerceptron.enegExp_ofReal line 118
  7. lemma OAI.IsingPerceptron.poissonTotal_enlaplace line 123
  8. lemma OAI.IsingPerceptron.enegExp_mul_total_ae line 135
  9. lemma OAI.IsingPerceptron.poissonFactorial_power_laplace line 143
  10. def OAI.IsingPerceptron.poissonPartitionNumerator line 178
  11. def OAI.IsingPerceptron.partitionCoefficient line 183
  12. def OAI.IsingPerceptron.partitionTimeIntegral line 186
  13. theorem OAI.IsingPerceptron.poissonPartitionNumerator_eq line 190
  14. lemma OAI.IsingPerceptron.partitionCoefficient_ofReal line 232
  15. lemma OAI.IsingPerceptron.sum_increment_entry line 244
  16. lemma OAI.IsingPerceptron.gamma_product_increment line 251
  17. lemma OAI.IsingPerceptron.partitionCoefficient_increment line 270
  18. theorem OAI.IsingPerceptron.poissonPartitionNumerator_increment line 294
  19. def OAI.IsingPerceptron.Marked.PoissonGood line 320
  20. lemma OAI.IsingPerceptron.Marked.poissonGood_ae line 323
  21. lemma OAI.IsingPerceptron.Marked.sigmaPart_eq_of_good line 334
  22. lemma OAI.IsingPerceptron.Marked.PoissonGood.dirac_add line 346
  23. def OAI.IsingPerceptron.Marked.poissonFactorial line 352
  24. lemma OAI.IsingPerceptron.Marked.measurable_fin_cons_param line 360
  25. lemma OAI.IsingPerceptron.Marked.measurable_poissonFactorial_param line 370
  26. lemma OAI.IsingPerceptron.Marked.poissonFactorial_dirac_add line 394
  27. def OAI.IsingPerceptron.Marked.poissonLaplaceWeight line 431
  28. lemma OAI.IsingPerceptron.Marked.measurable_poissonLaplaceWeight line 435
  29. lemma OAI.IsingPerceptron.Marked.poissonLaplaceWeight_dirac_add line 440
  30. lemma OAI.IsingPerceptron.Marked.measurable_poissonFactorial_body line 447
  31. lemma OAI.IsingPerceptron.Marked.poissonFactorial_laplace_step line 462
  32. theorem OAI.IsingPerceptron.Marked.poissonFactorial_laplace line 500
  33. def OAI.IsingPerceptron.markedPoissonTotal line 526
  34. lemma OAI.IsingPerceptron.measurable_markedPoissonTotal line 529
  35. lemma OAI.IsingPerceptron.markedPoissonTotal_eq line 533
  36. lemma OAI.IsingPerceptron.markedPoissonLaw_fst line 538
  37. lemma OAI.IsingPerceptron.markedPoissonTotal_positive line 545
  38. lemma OAI.IsingPerceptron.markedPoissonTotal_enlaplace line 553
  39. lemma OAI.IsingPerceptron.markedPoissonTotal_enegExp_ae line 566
  40. lemma OAI.IsingPerceptron.markedPower_fiber_null line 577
  41. lemma OAI.IsingPerceptron.marked_power_moment_laplace line 584
  42. lemma OAI.IsingPerceptron.markedFactorial_power_laplace line 615