OAI/Probability/IsingPerceptron/MarkedPartitionNumerator.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Marked Partition Numerator.

  1. def OAI.IsingPerceptron.markedPartitionNumerator line 15
  2. theorem OAI.IsingPerceptron.markedPartitionNumerator_eq line 22
  3. lemma OAI.IsingPerceptron.poissonLaw_ae_intensity line 77
  4. def OAI.IsingPerceptron.weightedPoissonTotal line 86
  5. lemma OAI.IsingPerceptron.measurable_weightedPoissonTotal line 90
  6. lemma OAI.IsingPerceptron.weightedPoissonTotal_real_eq_ae line 95
  7. lemma OAI.IsingPerceptron.weightedPower_laplace_cost line 113
  8. lemma OAI.IsingPerceptron.weightedPoissonTotal_laplace line 134
  9. structure OAI.IsingPerceptron.RawTreeSpace line 153
  10. def OAI.IsingPerceptron.rawTreeSpace line 159
  11. abbrev OAI.IsingPerceptron.RawTree line 163
  12. instance OAI.IsingPerceptron.rawTreeMeasurableSpace line 165
  13. instance OAI.IsingPerceptron.rawTreeNonempty line 168
  14. def OAI.IsingPerceptron.rawTreeTotal line 172
  15. lemma OAI.IsingPerceptron.measurable_rawTreeTotal line 176
  16. def OAI.IsingPerceptron.rawCascadeLaw line 188
  17. lemma OAI.IsingPerceptron.rawCascadeLaw_succ line 197
  18. lemma OAI.IsingPerceptron.rawTreeTotal_succ line 202
  19. def OAI.IsingPerceptron.HasStableTotal line 205
  20. lemma OAI.IsingPerceptron.HasStableTotal.finite_positive line 210
  21. lemma OAI.IsingPerceptron.HasStableTotal.real_laplace line 217
  22. lemma OAI.IsingPerceptron.HasStableTotal.positive_moment line 231
  23. lemma OAI.IsingPerceptron.HasStableTotal.negative_moment line 239
  24. lemma OAI.IsingPerceptron.weightedPoissonTotal_stable line 248
  25. def OAI.IsingPerceptron.CascadeExponents line 278
  26. lemma OAI.IsingPerceptron.CascadeExponents.tail line 281
  27. theorem OAI.IsingPerceptron.rawCascade_total_moments line 285
  28. theorem OAI.IsingPerceptron.rawCascade_total_log_square line 315
  29. lemma OAI.IsingPerceptron.measurable_withDensity_fixed line 334
  30. def OAI.IsingPerceptron.normalizeMass line 342
  31. lemma OAI.IsingPerceptron.measurable_normalizeMass line 347
  32. instance OAI.IsingPerceptron.normalizeMass_probability line 357
  33. def OAI.IsingPerceptron.childMass line 366
  34. lemma OAI.IsingPerceptron.childMass_univ line 369
  35. lemma OAI.IsingPerceptron.measurable_childMass line 373
  36. def OAI.IsingPerceptron.rawChildKernel line 378
  37. instance OAI.IsingPerceptron.rawChildKernel_markov line 381
  38. def OAI.IsingPerceptron.RawLeaf line 384
  39. instance OAI.IsingPerceptron.rawLeafMeasurableSpace line 388
  40. instance OAI.IsingPerceptron.rawLeafNonempty line 393
  41. def OAI.IsingPerceptron.rawLeafKernelData line 398
  42. def OAI.IsingPerceptron.rawLeafKernel line 409
  43. instance OAI.IsingPerceptron.rawLeafKernel_markov line 411
  44. lemma OAI.IsingPerceptron.rawLeafKernel_succ line 414
  45. lemma OAI.IsingPerceptron.rawChildKernel_lintegral line 417
  46. lemma OAI.IsingPerceptron.rawLeafKernel_lintegral line 431
  47. lemma OAI.IsingPerceptron.weightedPoissonTotal_enlaplace line 455
  48. lemma OAI.IsingPerceptron.weighted_power_moment_laplace line 470
  49. lemma OAI.IsingPerceptron.weightedFactorial_power_laplace line 515
  50. lemma OAI.IsingPerceptron.weightedPoissonTotal_enegExp_ae line 551
  51. def OAI.IsingPerceptron.weightedPartitionNumerator line 564
  52. def OAI.IsingPerceptron.weightedPartitionTimeIntegral line 572
  53. theorem OAI.IsingPerceptron.weightedPartitionNumerator_eq line 576