OAI/Probability/IsingPerceptron/BoundedTiltAverage.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Bounded Tilt Average.

  1. lemma OAI.IsingPerceptron.exp_mul_integrable_of_bound line 16
  2. lemma OAI.IsingPerceptron.integral_pos_exp_of_bound line 27
  3. lemma OAI.IsingPerceptron.bounded_tilted_integral_abs line 34
  4. lemma OAI.IsingPerceptron.integral_tilted_eq_div line 47
  5. def OAI.IsingPerceptron.gaussianTiltAverage line 55
  6. lemma OAI.IsingPerceptron.gaussianTiltAverage_abs_le line 58
  7. lemma OAI.IsingPerceptron.gaussianTiltAverage_zero line 65
  8. lemma OAI.IsingPerceptron.gaussianTiltAverage_eq_div line 69
  9. lemma OAI.IsingPerceptron.bounded_integrable line 85
  10. lemma OAI.IsingPerceptron.bounded_integral_hasDerivAt line 90
  11. lemma OAI.IsingPerceptron.bounded_exp_integral_hasDerivAt line 102
  12. lemma OAI.IsingPerceptron.gaussianTransform_hasDerivAt line 121
  13. lemma OAI.IsingPerceptron.bounded_exp_mul_integrable line 171
  14. lemma OAI.IsingPerceptron.bounded_tilt_hasDerivAt line 185
  15. lemma OAI.IsingPerceptron.gaussianTiltAverage_hasDerivAt line 252
  16. lemma OAI.IsingPerceptron.bounded_generator line 280
  17. lemma OAI.IsingPerceptron.gaussian_tilted_ibp line 287
  18. lemma OAI.IsingPerceptron.bounded_expIntegral_hasFDerivAt line 347
  19. lemma OAI.IsingPerceptron.bounded_logIntegral_hasFDerivAt line 371
  20. lemma OAI.IsingPerceptron.bounded_average_hasFDerivAt line 394
  21. lemma OAI.IsingPerceptron.gaussianTransform_abs_le line 434
  22. lemma OAI.IsingPerceptron.measurable_gaussianTransform_param line 469
  23. lemma OAI.IsingPerceptron.measurable_gaussianTiltAverage_param line 483
  24. def OAI.IsingPerceptron.pairLinear line 507
  25. lemma OAI.IsingPerceptron.pairLinear_apply line 510
  26. lemma OAI.IsingPerceptron.norm_pairLinear_le line 513
  27. lemma OAI.IsingPerceptron.measurable_pairLinear line 520
  28. lemma OAI.IsingPerceptron.integral_pairLinear line 524
  29. lemma OAI.IsingPerceptron.integrable_tilt_of_bound line 530
  30. lemma OAI.IsingPerceptron.abs_div_two_sqrt_le line 556
  31. lemma OAI.IsingPerceptron.affine_gaussian_shift_hasFDerivAt line 562
  32. lemma OAI.IsingPerceptron.gaussianFamily_raw_hasFDerivAt line 580