OAI/Probability/Perceptron/Variational/EntropicHeat.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.integrable_of_all_exp line 15
  2. lemma OAI.SphericalPerceptronFreeEnergy.all_exp_add_const line 20
  3. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_add_const line 25
  4. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_mono_variable line 37
  5. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_bounded_difference line 50
  6. def OAI.SphericalPerceptronFreeEnergy.gaussianEntropic line 75
  7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_lipschitz line 78
  8. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_mono_parameter line 90
  9. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_zero line 95
  10. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_pos line 100
  11. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_mono line 105
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_add_const line 113
  13. def OAI.SphericalPerceptronFreeEnergy.gaussianEntropicParamConstant line 118
  14. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropicParamConstant_nonneg line 122
  15. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_parameter_bound line 129