OAI/Probability/Perceptron/Variational/RoundedMarkedSelection.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.unitQuantileField line 13
  2. def OAI.SphericalPerceptronFreeEnergy.strictRoundModel line 16
  3. lemma OAI.SphericalPerceptronFreeEnergy.strictRoundModel_strict line 19
  4. def OAI.SphericalPerceptronFreeEnergy.roundTimeValue line 23
  5. lemma OAI.SphericalPerceptronFreeEnergy.roundTimeValue_mono line 27
  6. def OAI.SphericalPerceptronFreeEnergy.roundTime line 30
  7. lemma OAI.SphericalPerceptronFreeEnergy.roundTime_mono line 33
  8. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.round_tendsto line 36
  9. lemma OAI.SphericalPerceptronFreeEnergy.roundTime_tendsto line 43
  10. def OAI.SphericalPerceptronFreeEnergy.roundedPairCoeff line 47
  11. lemma OAI.SphericalPerceptronFreeEnergy.roundedPairCoeff_bounds line 54
  12. def OAI.SphericalPerceptronFreeEnergy.roundedPairFunction line 64
  13. lemma OAI.SphericalPerceptronFreeEnergy.roundedPairFunction_mono line 67
  14. lemma OAI.SphericalPerceptronFreeEnergy.roundedPairFunction_bounds line 71
  15. lemma OAI.SphericalPerceptronFreeEnergy.roundedPairFunction_agrees line 76
  16. lemma OAI.SphericalPerceptronFreeEnergy.roundedPair_selection line 84
  17. lemma OAI.SphericalPerceptronFreeEnergy.roundedPair_sum_integral line 91
  18. lemma OAI.SphericalPerceptronFreeEnergy.roundedPair_sum_tendsto line 105
  19. lemma OAI.SphericalPerceptronFreeEnergy.roundTime_sum_integral line 130
  20. lemma OAI.SphericalPerceptronFreeEnergy.roundTime_sum_tendsto line 141