OAI/Probability/SphericalField/Heat/Entropic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.integrable_of_all_exp line 18
  2. lemma OAI.SphericalPerceptron.all_exp_add_const line 23
  3. lemma OAI.SphericalPerceptron.entropicMean_add_const line 28
  4. lemma OAI.SphericalPerceptron.entropicMean_mono_variable line 40
  5. lemma OAI.SphericalPerceptron.entropicMean_bounded_difference line 53
  6. def OAI.SphericalPerceptron.gaussianEntropic line 79
  7. lemma OAI.SphericalPerceptron.gaussianEntropic_lipschitz line 82
  8. lemma OAI.SphericalPerceptron.gaussianEntropic_mono_parameter line 94
  9. lemma OAI.SphericalPerceptron.gaussianEntropic_zero line 99
  10. lemma OAI.SphericalPerceptron.gaussianEntropic_pos line 104
  11. lemma OAI.SphericalPerceptron.gaussianEntropic_mono line 109
  12. lemma OAI.SphericalPerceptron.gaussianEntropic_add_const line 117
  13. def OAI.SphericalPerceptron.gaussianEntropicParamConstant line 122
  14. lemma OAI.SphericalPerceptron.gaussianEntropicParamConstant_nonneg line 126
  15. lemma OAI.SphericalPerceptron.gaussianEntropic_parameter_bound line 133