OAI/Probability/IsingPerceptron/ChildLabel.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Child Label.

  1. abbrev OAI.IsingPerceptron.ChildLabel line 14
  2. abbrev OAI.IsingPerceptron.WeightCloud line 15
  3. def OAI.IsingPerceptron.labeledTreeSpace line 17
  4. abbrev OAI.IsingPerceptron.LabeledTree line 23
  5. instance OAI.IsingPerceptron.labeledTreeMeasurableSpace line 24
  6. instance OAI.IsingPerceptron.labeledTreeNonempty line 26
  7. def OAI.IsingPerceptron.intensityComponents line 31
  8. lemma OAI.IsingPerceptron.intensityComponents_sum line 34
  9. def OAI.IsingPerceptron.labeledCascadeLaw line 38
  10. def OAI.IsingPerceptron.labeledTreeForget line 49
  11. lemma OAI.IsingPerceptron.measurable_labeledTreeForget line 53
  12. theorem OAI.IsingPerceptron.labeledCascadeLaw_forget line 62
  13. def OAI.IsingPerceptron.LabeledLeaf line 101
  14. instance OAI.IsingPerceptron.labeledLeafMeasurableSpace line 104
  15. instance OAI.IsingPerceptron.labeledLeafCountable line 108
  16. instance OAI.IsingPerceptron.labeledLeafSingleton line 112
  17. instance OAI.IsingPerceptron.labeledLeafNonempty line 116
  18. def OAI.IsingPerceptron.childLabelWeight line 121
  19. def OAI.IsingPerceptron.labeledLeafWeight line 124
  20. lemma OAI.IsingPerceptron.measurable_childLabelWeight line 128
  21. lemma OAI.IsingPerceptron.measurable_labeledLeafWeight line 135
  22. def OAI.IsingPerceptron.labeledLeafMass line 144
  23. lemma OAI.IsingPerceptron.labeledLeafMass_lintegral line 147
  24. lemma OAI.IsingPerceptron.measurable_labeledLeafMass line 153
  25. lemma OAI.IsingPerceptron.finiteCloud_tsum_weight line 162
  26. lemma OAI.IsingPerceptron.rawTreeTotal_labeled_eq line 177
  27. lemma OAI.IsingPerceptron.labeledLeafMass_univ line 195
  28. def OAI.IsingPerceptron.labeledLeafLaw line 200
  29. instance OAI.IsingPerceptron.labeledLeafLaw_probability line 202
  30. lemma OAI.IsingPerceptron.measurable_labeledLeafLaw line 204
  31. def OAI.IsingPerceptron.markForestSpace line 209
  32. abbrev OAI.IsingPerceptron.MarkForest line 215
  33. instance OAI.IsingPerceptron.markForestMeasurableSpace line 216
  34. instance OAI.IsingPerceptron.markForestNonempty line 218
  35. def OAI.IsingPerceptron.markForestLaw line 223
  36. def OAI.IsingPerceptron.labeledNoiseJoin line 232
  37. lemma OAI.IsingPerceptron.measurable_labeledNoiseJoin line 237
  38. lemma OAI.IsingPerceptron.infinitePi_prod_join2 line 253
  39. lemma OAI.IsingPerceptron.measurePreserving_swap_first_two line 267
  40. theorem OAI.IsingPerceptron.labeledNoiseJoin_law line 277
  41. lemma OAI.IsingPerceptron.infinitePi_option_join line 342
  42. lemma OAI.IsingPerceptron.infinitePi_option_split line 390
  43. lemma OAI.IsingPerceptron.infinitePi_triple_curry line 402
  44. def OAI.IsingPerceptron.ForestVertex line 417
  45. instance OAI.IsingPerceptron.forestVertexCountable line 421
  46. def OAI.IsingPerceptron.forestVertexDepth line 426
  47. def OAI.IsingPerceptron.markForestOfCoords line 433
  48. lemma OAI.IsingPerceptron.measurable_markForestOfCoords line 437
  49. theorem OAI.IsingPerceptron.markForestOfCoords_law line 448
  50. theorem OAI.IsingPerceptron.labeledNoiseCoordinates_law line 497
  51. theorem OAI.IsingPerceptron.labeledGaussianCoordinates_law line 514
  52. lemma OAI.IsingPerceptron.labeledMarkedMeasure_lintegral line 543
  53. lemma OAI.IsingPerceptron.labeledMarkedMeasure_ae line 550
  54. def OAI.IsingPerceptron.labeledNoiseLeaf line 561
  55. lemma OAI.IsingPerceptron.measurable_labeledNoiseLeaf line 567
  56. theorem OAI.IsingPerceptron.labeledLeafMass_noiseMap line 580
  57. theorem OAI.IsingPerceptron.labeledLeafLaw_noiseMap line 635