OAI/Probability/Perceptron/Variational/IndexedVisit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.oneDecoratedVisit line 16
  2. lemma OAI.SphericalPerceptronFreeEnergy.oneDecoratedVisit_valid line 20
  3. lemma OAI.SphericalPerceptronFreeEnergy.oneDecoratedVisit_count line 26
  4. lemma OAI.SphericalPerceptronFreeEnergy.oneDecoratedVisit_likelihood line 32
  5. def OAI.SphericalPerceptronFreeEnergy.indexedOneVisit line 46
  6. lemma OAI.SphericalPerceptronFreeEnergy.indexedOneVisit_measurable line 51
  7. lemma OAI.SphericalPerceptronFreeEnergy.indexedOneVisit_zero line 61
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedOneVisit_succ line 68
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedOneVisit_eq_shape line 78
  10. def OAI.SphericalPerceptronFreeEnergy.twoDecoratedVisit line 125
  11. lemma OAI.SphericalPerceptronFreeEnergy.twoDecoratedVisit_valid line 130
  12. lemma OAI.SphericalPerceptronFreeEnergy.twoDecoratedVisit_count line 147
  13. lemma OAI.SphericalPerceptronFreeEnergy.activeRoot_eq_iff line 156
  14. lemma OAI.SphericalPerceptronFreeEnergy.indexedCommonDepth_active_zero line 167
  15. lemma OAI.SphericalPerceptronFreeEnergy.indexedCommonDepth_active_succ line 174
  16. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltedPair_tsum_succ line 185
  17. def OAI.SphericalPerceptronFreeEnergy.indexedTwoVisit line 212
  18. lemma OAI.SphericalPerceptronFreeEnergy.indexedTwoVisit_measurable line 220
  19. lemma OAI.SphericalPerceptronFreeEnergy.indexedTwoVisit_zero line 240
  20. lemma OAI.SphericalPerceptronFreeEnergy.indexedTwoVisit_succ_zero line 248
  21. lemma OAI.SphericalPerceptronFreeEnergy.indexedTwoVisit_succ_succ line 279