OAI/Probability/Perceptron/Variational/StableLaplaceConstant.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.finitePointMeasure_insertNth line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.finite_point_mecke line 21
  3. lemma OAI.SphericalPerceptronFreeEnergy.poissonMeasure_succ_mul line 48
  4. lemma OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_mecke line 61
  5. def OAI.SphericalPerceptronFreeEnergy.stableLaplaceConstant line 116
  6. lemma OAI.SphericalPerceptronFreeEnergy.one_sub_exp_neg_le_min line 119
  7. lemma OAI.SphericalPerceptronFreeEnergy.stableLaplaceConstant_finite line 125
  8. lemma OAI.SphericalPerceptronFreeEnergy.stableLaplaceConstant_positive line 132
  9. lemma OAI.SphericalPerceptronFreeEnergy.stableLaplaceExponent_scaling line 145
  10. def OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal line 158
  11. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_measurable line 161
  12. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_pos line 164
  13. lemma OAI.SphericalPerceptronFreeEnergy.stablePoissonTotal_laplace line 169
  14. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_integrationByParts line 190
  15. def OAI.SphericalPerceptronFreeEnergy.tiltIntegral line 218
  16. def OAI.SphericalPerceptronFreeEnergy.tiltPartition line 220
  17. def OAI.SphericalPerceptronFreeEnergy.tiltMean line 222
  18. lemma OAI.SphericalPerceptronFreeEnergy.tilt_integrable line 224
  19. lemma OAI.SphericalPerceptronFreeEnergy.tilt_integral_deriv line 235
  20. lemma OAI.SphericalPerceptronFreeEnergy.tilt_partition_pos line 264
  21. lemma OAI.SphericalPerceptronFreeEnergy.tilt_partition_deriv line 279
  22. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_deriv line 290
  23. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_bound line 302
  24. def OAI.SphericalPerceptronFreeEnergy.tiltLaw line 324
  25. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_probability line 328
  26. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_integral line 340
  27. lemma OAI.SphericalPerceptronFreeEnergy.tilt_mean_continuous line 350
  28. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_tilt_integrationByParts line 356
  29. def OAI.SphericalPerceptronFreeEnergy.replicaPotential line 384
  30. lemma OAI.SphericalPerceptronFreeEnergy.replicaPotential_measurable line 386
  31. lemma OAI.SphericalPerceptronFreeEnergy.replicaPotential_bound line 390
  32. lemma OAI.SphericalPerceptronFreeEnergy.replica_partition line 400
  33. lemma OAI.SphericalPerceptronFreeEnergy.replica_mean_potential line 408