OAI/Probability/Perceptron/Variational/GaussianAverage.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.controlValue_trial_sub_le line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.controlValue_trial_abs_sub_le line 28
  3. lemma OAI.SphericalPerceptronFreeEnergy.usual_measurable_aemeasurable line 37
  4. lemma OAI.SphericalPerceptronFreeEnergy.brownian_increment_indep_adapted line 43
  5. lemma OAI.SphericalPerceptronFreeEnergy.second_order_taylor_bound line 49
  6. lemma OAI.SphericalPerceptronFreeEnergy.first_order_taylor_bound line 78
  7. lemma OAI.SphericalPerceptronFreeEnergy.smooth_deriv_lipschitz line 100
  8. lemma OAI.SphericalPerceptronFreeEnergy.drift_shift_taylor_bound line 107
  9. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_abs_moment line 122
  10. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_law_integrable_abs_pow line 134
  11. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_law_sq_mean line 144
  12. lemma OAI.SphericalPerceptronFreeEnergy.bounded_real_integrable line 154
  13. lemma OAI.SphericalPerceptronFreeEnergy.boundedContinuousFunction_integrable_comp line 159
  14. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_taylor_mean_bound line 165
  15. lemma OAI.SphericalPerceptronFreeEnergy.drift_shift_mean_bound line 232
  16. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_drift_taylor_mean_bound line 282
  17. def OAI.SphericalPerceptronFreeEnergy.gaussianAverage line 306
  18. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_integrable line 309
  19. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_abs_le line 313
  20. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_continuous line 319
  21. def OAI.SphericalPerceptronFreeEnergy.gaussianAverageBCF line 327
  22. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverageBCF_coe line 334
  23. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_zero line 337
  24. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_semigroup line 340
  25. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_hasDerivAt line 349
  26. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_deriv line 361
  27. lemma OAI.SphericalPerceptronFreeEnergy.exp_bcf_bound line 366
  28. def OAI.SphericalPerceptronFreeEnergy.expBCF line 376
  29. lemma OAI.SphericalPerceptronFreeEnergy.expBCF_apply line 382
  30. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_exp_pos line 385
  31. lemma OAI.SphericalPerceptronFreeEnergy.gaussianAverage_exp_bounds line 392
  32. def OAI.SphericalPerceptronFreeEnergy.heatLog line 406
  33. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_abs_le line 409