OAI/Probability/Perceptron/Variational/OrderedCode.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.orderedLevelCode line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.orderedLevelCode_mono line 14
  3. lemma OAI.SphericalPerceptronFreeEnergy.orderedLevelCode_value line 22
  4. lemma OAI.SphericalPerceptronFreeEnergy.orderedLevelCode_top line 31
  5. lemma OAI.SphericalPerceptronFreeEnergy.orderedLevelCode_measurable line 36
  6. lemma OAI.SphericalPerceptronFreeEnergy.roundLower_one line 39
  7. lemma OAI.SphericalPerceptronFreeEnergy.orderedRoundCode_label line 44
  8. lemma OAI.SphericalPerceptronFreeEnergy.orderedRoundCode_one line 52
  9. lemma OAI.SphericalPerceptronFreeEnergy.compactGG_events_general line 59
  10. def OAI.SphericalPerceptronFreeEnergy.finiteCodeArray line 103
  11. def OAI.SphericalPerceptronFreeEnergy.finiteCodeBlock line 106
  12. lemma OAI.SphericalPerceptronFreeEnergy.finiteCodeArray_measurable line 111
  13. lemma OAI.SphericalPerceptronFreeEnergy.finiteCodeBlock_measurable line 119
  14. lemma OAI.SphericalPerceptronFreeEnergy.compactGG_finite_pushforward_general line 125