OAI/Probability/Perceptron/Variational/GaussianEnergyMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonian_energy_combine line 21
2. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonian_energy_exp_integrable line 31
3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonian_energy_exp_bound line 40
4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_weighted_moment_integrable line 57
5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_weighted_moment_bound line 74
6. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_weighted_moment_joint_integrable line 103
7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEnergy_tail_weighted_L2 line 114
8. lemma OAI.SphericalPerceptronFreeEnergy.integral_mul_le_sqrt_integrals line 141
9. lemma OAI.SphericalPerceptronFreeEnergy.tiltPartition_joint_measurable line 159
10. lemma OAI.SphericalPerceptronFreeEnergy.weighted_gibbs_L1_integrable line 164
11. lemma OAI.SphericalPerceptronFreeEnergy.tiltMean_abs_eq_weighted_integral line 179
12. lemma OAI.SphericalPerceptronFreeEnergy.tiltMean_abs_annealed_integrable line 189
13. lemma OAI.SphericalPerceptronFreeEnergy.tiltMean_abs_annealed_L2_bound line 195