OAI/Probability/Perceptron/Variational/GaussianBoltzmann.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.integrable_prod_of_nonneg_uniform_integral line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.exp_square_sub_bound line 28
  3. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianField_exp_joint_integrable line 40
  4. lemma OAI.SphericalPerceptronFreeEnergy.truncatedCountableGaussianField_exp_joint_integrable line 49
  5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBoltzmann_difference_sq_integrable line 60
  6. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBoltzmann_difference_sq_integral_le line 74
  7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBoltzmann_difference_sq_joint_integrable line 97
  8. lemma OAI.SphericalPerceptronFreeEnergy.gaussianBoltzmann_truncation_L2 line 106
  9. def OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian line 129
  10. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian_measurable line 132
  11. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian_exp_integrable line 143
  12. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian_exp_integral_bound line 150
  13. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian_exp_joint_integrable line 162
  14. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian_joint_integrable line 172
  15. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianHamiltonian_exp_double_integral_bound line 180
  16. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonianPartition_measurable line 190
  17. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonianPartition_pos_ae line 196
  18. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonianPartition_inverse_power_integrable line 202
  19. lemma OAI.SphericalPerceptronFreeEnergy.gaussianHamiltonianPartition_inverse_power_bound line 216