OAI/Probability/SphericalField/Gibbs/Tilting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.tiltIntegral line 19
  2. def OAI.SphericalPerceptron.tiltPartition line 21
  3. def OAI.SphericalPerceptron.tiltMean line 23
  4. lemma OAI.SphericalPerceptron.tilt_integrable line 25
  5. lemma OAI.SphericalPerceptron.tilt_integral_deriv line 36
  6. lemma OAI.SphericalPerceptron.tilt_partition_pos line 65
  7. lemma OAI.SphericalPerceptron.tilt_partition_deriv line 80
  8. lemma OAI.SphericalPerceptron.tilt_mean_deriv line 91
  9. lemma OAI.SphericalPerceptron.tilt_mean_bound line 103
  10. def OAI.SphericalPerceptron.tiltLaw line 125
  11. lemma OAI.SphericalPerceptron.tilt_law_probability line 129
  12. lemma OAI.SphericalPerceptron.tilt_law_integral line 141
  13. lemma OAI.SphericalPerceptron.tilt_mean_continuous line 151
  14. lemma OAI.SphericalPerceptron.gaussian_tilt_integrationByParts line 157
  15. def OAI.SphericalPerceptron.replicaPotential line 185
  16. lemma OAI.SphericalPerceptron.replicaPotential_measurable line 187
  17. lemma OAI.SphericalPerceptron.replicaPotential_bound line 191