OAI/Probability/Perceptron/Variational/DensityLipschitz.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.poissonRealMean_increment_bound line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.poissonRealMean_lipschitz_bound line 22
  3. lemma OAI.SphericalPerceptronFreeEnergy.sourceExpectedPressure_density_comparison line 33
  4. lemma OAI.SphericalPerceptronFreeEnergy.enrichedFeatureBound_continuous line 52
  5. lemma OAI.SphericalPerceptronFreeEnergy.sourceFieldDistance_joint_continuous line 58
  6. abbrev OAI.SphericalPerceptronFreeEnergy.SourceContactParameter line 77
  7. def OAI.SphericalPerceptronFreeEnergy.sourceContactDomain line 79
  8. def OAI.SphericalPerceptronFreeEnergy.sourceJointPressure line 82
  9. def OAI.SphericalPerceptronFreeEnergy.sourceContactDistance line 86
  10. lemma OAI.SphericalPerceptronFreeEnergy.sourceContactDistance_continuous line 91
  11. lemma OAI.SphericalPerceptronFreeEnergy.sourceContactDistance_self line 108
  12. lemma OAI.SphericalPerceptronFreeEnergy.sourceJointPressure_comparison line 112
  13. lemma OAI.SphericalPerceptronFreeEnergy.sourceJointPressure_continuousOn line 135