OAI/Probability/Perceptron/Variational/ShapeSampleLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.indexedShiftSum_zero line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltedWeight_zero line 18
  3. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltedTotal_zero line 23
  4. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafMeasure_singleton line 29
  5. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltedProbability_zero line 36
  6. def OAI.SphericalPerceptronFreeEnergy.indexedSampleShape line 45
  7. lemma OAI.SphericalPerceptronFreeEnergy.indexedSampleShape_measurable line 50
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedSampleShape_eq_measure line 58
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedShapeVisit_zero_eq_sample line 72
  10. theorem OAI.SphericalPerceptronFreeEnergy.indexedSampleShape_integral line 83
  11. def OAI.SphericalPerceptronFreeEnergy.cascadeShapeFocus line 108
  12. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeFocus_cons line 115
  13. def OAI.SphericalPerceptronFreeEnergy.indexedClassMass line 122
  14. lemma OAI.SphericalPerceptronFreeEnergy.indexedClassMass_measurable line 129
  15. lemma OAI.SphericalPerceptronFreeEnergy.indexedClassMass_active_succ line 138
  16. def OAI.SphericalPerceptronFreeEnergy.indexedFocusedVisit line 163
  17. lemma OAI.SphericalPerceptronFreeEnergy.indexedFocusedVisit_measurable line 172