OAI/Probability/Perceptron/Variational/EntropicParameter.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.mem_interior_integrableExpSet_of_all line 17
  2. lemma OAI.SphericalPerceptronFreeEnergy.cgf_analytic_of_all line 24
  3. lemma OAI.SphericalPerceptronFreeEnergy.cgf_second_nonneg line 29
  4. lemma OAI.SphericalPerceptronFreeEnergy.cgf_deriv_monotone line 39
  5. def OAI.SphericalPerceptronFreeEnergy.entropicMean line 45
  6. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_eq_div line 48
  7. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_zero line 58
  8. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_monotone line 62
  9. lemma OAI.SphericalPerceptronFreeEnergy.entropicMean_param_bound line 73
  10. lemma OAI.SphericalPerceptronFreeEnergy.cgf_second_le_of_moments line 110
  11. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_integrable_exp_norm line 129
  12. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_integrable_norm_sq_exp line 141
  13. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_integrable_exp_lipschitz line 149
  14. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_integrable_lipschitz line 168