OAI/Probability/Perceptron/Variational/BcfEvalRingHom.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.shiftBCF_gaussian_integrable line 20
  2. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_scaling line 27
  3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverageBCF_scaling line 37
  4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverageBCF_time_hasDerivAt line 46
  5. lemma OAI.SphericalPerceptronFreeEnergy.log_lipschitz_above line 116
  6. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_time_continuousAt line 124
  7. def OAI.SphericalPerceptronFreeEnergy.bcfEvalRingHom line 154
  8. lemma OAI.SphericalPerceptronFreeEnergy.expBCF_eq_normedSpace_exp line 161
  9. lemma OAI.SphericalPerceptronFreeEnergy.expBCF_hasFDerivAt line 170
  10. def OAI.SphericalPerceptronFreeEnergy.heatGenerator line 179
  11. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_time_hasDerivAt line 182
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverageBCF_scaling_of_deriv line 234
  13. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverageBCF_time_continuous_of_deriv line 244
  14. lemma OAI.SphericalPerceptronFreeEnergy.heatTiltBCF_time_continuous_of_deriv line 263
  15. lemma OAI.SphericalPerceptronFreeEnergy.heatGenerator_hasDerivAt line 312
  16. lemma OAI.SphericalPerceptronFreeEnergy.heatTilt_heatGenerator line 320
  17. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_moving_hasDerivAt line 356
  18. lemma OAI.SphericalPerceptronFreeEnergy.heatTiltBCF_hasDerivAt line 408