OAI/Probability/Perceptron/Variational/TiltedPathDiagonal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_last line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.pathCorrelation_le_diagonal line 32
  3. def OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation line 47
  4. def OAI.SphericalPerceptronFreeEnergy.rootPathMean line 50
  5. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_integrable line 53
  6. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_nonneg line 61
  7. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_monotone line 67
  8. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_bound line 77
  9. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_le_diagonal line 86
  10. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_one line 97
  11. lemma OAI.SphericalPerceptronFreeEnergy.rootPathCorrelation_parallel line 102
  12. def OAI.SphericalPerceptronFreeEnergy.residualResponse line 118
  13. lemma OAI.SphericalPerceptronFreeEnergy.residualResponse_eq_tiltMean line 121
  14. lemma OAI.SphericalPerceptronFreeEnergy.residualResponse_continuous line 127
  15. lemma OAI.SphericalPerceptronFreeEnergy.residualResponse_bound line 133
  16. def OAI.SphericalPerceptronFreeEnergy.residualResponseBCF line 140
  17. lemma OAI.SphericalPerceptronFreeEnergy.residualResponseBCF_apply line 148
  18. lemma OAI.SphericalPerceptronFreeEnergy.residualResponse_weighted line 151
  19. lemma OAI.SphericalPerceptronFreeEnergy.residualResponse_jensen line 157
  20. lemma OAI.SphericalPerceptronFreeEnergy.residualResponse_one line 174