OAI/Probability/Perceptron/Variational/ContactGGRate.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.contact_gg_rate_identity line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.contact_gg_rate_bound line 37
  3. lemma OAI.SphericalPerceptronFreeEnergy.perturbationAmplitude_product line 53
  4. lemma OAI.SphericalPerceptronFreeEnergy.contact_gg_rate_tendsto line 62
  5. lemma OAI.SphericalPerceptronFreeEnergy.source_contact_joint_gg_rate line 69
  6. def OAI.SphericalPerceptronFreeEnergy.gibbsKernelDensity line 111
  7. lemma OAI.SphericalPerceptronFreeEnergy.gibbsKernelDensity_measurable line 115
  8. def OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel line 122
  9. lemma OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel_of_integrable line 124
  10. lemma OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel_of_not_integrable line 134
  11. lemma OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel_markov line 143
  12. lemma OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel_replica_integral line 153
  13. lemma OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel_congr_apply line 160