OAI/Probability/Perceptron/Variational/GaussianGibbsEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.gaussianTailCoefficient_zero line 18
2. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_tail_tilt_integrable line 24
3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_tail_tilt_tendsto line 33
4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_tail_weighted_integrable_ae line 50
5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_tail_replica_integrable line 62
6. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_tail_replica_tendsto line 80
7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_replica_integrable line 109
8. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_replica_prefix_tendsto line 116