OAI/Probability/Perceptron/Cascade/IndexedCascadeRegular.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.indexedPoissonMeasure_lintegral line 11
  2. def OAI.SphericalPerceptronFreeEnergy.indexedCascadeRootMass line 18
  3. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeRootMass_measurable line 21
  4. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeRealize_rootMass line 25
  5. def OAI.SphericalPerceptronFreeEnergy.IndexedCascadeGood line 31
  6. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeBase_child_law line 36
  7. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeRootMass_pos line 49
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeGood_ae line 66
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeGood_countKernel line 80
  10. def OAI.SphericalPerceptronFreeEnergy.IndexedLeaf line 92
  11. instance OAI.SphericalPerceptronFreeEnergy.indexedLeaf_countable line 96
  12. instance OAI.SphericalPerceptronFreeEnergy.indexedLeaf_nonempty line 101
  13. instance OAI.SphericalPerceptronFreeEnergy.indexedLeaf_measurableSingleton line 106
  14. def OAI.SphericalPerceptronFreeEnergy.indexedLeafWeight line 111
  15. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafWeight_measurable line 117
  16. def OAI.SphericalPerceptronFreeEnergy.indexedLeafMeasure line 134
  17. instance OAI.SphericalPerceptronFreeEnergy.indexedLeafMeasure_sfinite line 137
  18. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafMeasure_measurable line 142
  19. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafMeasure_lintegral line 150
  20. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafMeasure_lintegral_succ line 154
  21. def OAI.SphericalPerceptronFreeEnergy.indexedLeafState line 184
  22. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafState_measurable line 190