OAI/Probability/Perceptron/Variational/IntegrableGibbs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.tilt_partition_pos_of_integrable line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_probability_of_integrable line 25
  3. lemma OAI.SphericalPerceptronFreeEnergy.tilt_law_integral_of_integrable line 34
  4. lemma OAI.SphericalPerceptronFreeEnergy.tiltMean_bound_of_integrable line 43
  5. lemma OAI.SphericalPerceptronFreeEnergy.exp_integral_le_of_integrable line 52
  6. lemma OAI.SphericalPerceptronFreeEnergy.inverse_partition_power_le line 58
  7. lemma OAI.SphericalPerceptronFreeEnergy.abs_le_exp_add_exp_neg line 78
  8. lemma OAI.SphericalPerceptronFreeEnergy.abs_pow_mul_exp_le line 85
  9. lemma OAI.SphericalPerceptronFreeEnergy.integrable_of_exp_pos_neg line 105
  10. lemma OAI.SphericalPerceptronFreeEnergy.coupling_mgf_identity line 116
  11. lemma OAI.SphericalPerceptronFreeEnergy.coupling_expSet line 124
  12. lemma OAI.SphericalPerceptronFreeEnergy.coupling_log_hasDerivAt line 132
  13. lemma OAI.SphericalPerceptronFreeEnergy.coupling_log_second_derivative line 161